diff options
| author | Josh Chen | 2020-05-24 20:44:33 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-05-24 20:44:33 +0200 |
| commit | 3ad2f03f7dbc922e2c711241146db091d193003d (patch) | |
| tree | 6db26730510b119bf10dc836d21a9869ace6c416 /spartan/theories/Equivalence.thy | |
| parent | 6f37e6b72905eff8f2c7078823e5577bc5b55eb0 (diff) | |
new work on elimination tactic
Diffstat (limited to '')
| -rw-r--r-- | spartan/theories/Equivalence.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/theories/Equivalence.thy b/spartan/theories/Equivalence.thy index 97cd18d..73f1e0d 100644 --- a/spartan/theories/Equivalence.thy +++ b/spartan/theories/Equivalence.thy @@ -276,7 +276,7 @@ Lemma (derive) biinv_imp_qinv: ultimately have "g ~ h" apply (rewrite to "g \<circ> (id B)" id_right[symmetric]) apply (rewrite to "(id A) \<circ> h" id_left[symmetric]) - by (rule homotopy_transitive) (assumption, typechk) + by (rule homotopy_transitive) (assumption+, typechk) then have "f \<circ> g ~ f \<circ> h" by (rule homotopy_funcomp_right) |