equal
deleted
inserted
replaced
142 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
142 (\<forall>x a. hom_m (Sig x a) = fsgm (\<lambda>y. hom_o ([(x, y)] \<bullet> a)) (\<lambda>y. [(x, y)] \<bullet> a)) |
143 )" |
143 )" |
144 apply (lifting tolift) |
144 apply (lifting tolift) |
145 apply (regularize) |
145 apply (regularize) |
146 apply (simp) |
146 apply (simp) |
147 prefer 2 |
|
148 apply cleaning |
|
149 apply (subst ex_prs) |
|
150 apply (tactic {* Quotient_Tacs.quotient_tac @{context} 1 *}) |
|
151 apply (rule refl) |
|
152 sorry |
147 sorry |
153 |
148 |
154 lemma tolift': |
149 lemma tolift': |
155 "\<forall> fvar. |
150 "\<forall> fvar. |
156 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |
151 \<forall> fobj\<in>Respects (op = ===> list_rel (prod_rel (op =) alpha_method) ===> op =). |