diff options
Diffstat (limited to 'spartan/theories/Equivalence.thy')
| -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) |