86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
86 | "bv_tvck (TVCKCons v k t) = {atom v} \<union> bv_tvck t" |
87 |
87 |
88 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
88 lemmas fv_supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.supp(1-9,11,13,15) |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
89 lemmas supp=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.fv[simplified fv_supp] |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
90 lemmas perm=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.perm |
|
91 lemmas eq_iff=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff |
|
92 lemmas inducts=tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.inducts |
91 |
93 |
92 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
94 lemma fresh_star_minus_perm: "as \<sharp>* - p = as \<sharp>* (p :: perm)" |
93 unfolding fresh_star_def Ball_def |
95 unfolding fresh_star_def Ball_def |
94 by auto (simp_all add: fresh_minus_perm) |
96 by auto (simp_all add: fresh_minus_perm) |
|
97 |
|
98 lemma fv_alpha1: "fv_bv_tvtk x \<sharp>* pa \<Longrightarrow> alpha_bv_tvtk (pa \<bullet> x) x" |
|
99 apply (induct x rule: inducts(11)) |
|
100 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
101 apply (simp_all add: eq_iff fresh_star_union) |
|
102 apply (subst supp_perm_eq) |
|
103 apply (simp_all add: fv_supp) |
|
104 done |
|
105 |
|
106 lemma fv_alpha2: "fv_bv_tvck x \<sharp>* pa \<Longrightarrow> alpha_bv_tvck (pa \<bullet> x) x" |
|
107 apply (induct x rule: inducts(12)) |
|
108 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
109 apply (simp_all add: eq_iff fresh_star_union) |
|
110 apply (subst supp_perm_eq) |
|
111 apply (simp_all add: fv_supp) |
|
112 done |
|
113 |
|
114 lemma fv_alpha3: "fv_bv_vt x \<sharp>* pa \<Longrightarrow> alpha_bv_vt (pa \<bullet> x) x" |
|
115 apply (induct x rule: inducts(10)) |
|
116 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
117 apply (simp_all add: eq_iff fresh_star_union) |
|
118 apply (subst supp_perm_eq) |
|
119 apply (simp_all add: fv_supp) |
|
120 done |
|
121 |
|
122 lemma fv_alpha: "fv_bv x \<sharp>* pa \<Longrightarrow> alpha_bv (pa \<bullet> x) x" |
|
123 apply (induct x rule: inducts(9)) |
|
124 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
125 apply (simp_all add: eq_iff fresh_star_union) |
|
126 apply (simp add: fv_alpha1 fv_alpha2 fv_alpha3) |
|
127 apply (simp add: eqvts) |
|
128 done |
|
129 |
|
130 lemma fin1: "finite (fv_bv_tvtk x)" |
|
131 apply (induct x rule: inducts(11)) |
|
132 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
133 apply (simp_all add: fv_supp finite_supp) |
|
134 done |
|
135 |
|
136 lemma fin2: "finite (fv_bv_tvck x)" |
|
137 apply (induct x rule: inducts(12)) |
|
138 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
139 apply (simp_all add: fv_supp finite_supp) |
|
140 done |
|
141 |
|
142 lemma fin3: "finite (fv_bv_vt x)" |
|
143 apply (induct x rule: inducts(10)) |
|
144 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
145 apply (simp_all add: fv_supp finite_supp) |
|
146 done |
|
147 |
|
148 lemma fin_fv_bv: "finite (fv_bv x)" |
|
149 apply (induct x rule: inducts(9)) |
|
150 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
151 apply (simp add: fin1 fin2 fin3) |
|
152 done |
|
153 |
|
154 lemma finb1: "finite (bv_tvtk x)" |
|
155 apply (induct x rule: inducts(11)) |
|
156 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
157 apply (simp_all add: fv_supp finite_supp) |
|
158 done |
|
159 |
|
160 lemma finb2: "finite (bv_tvck x)" |
|
161 apply (induct x rule: inducts(12)) |
|
162 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
163 apply (simp_all add: fv_supp finite_supp) |
|
164 done |
|
165 |
|
166 lemma finb3: "finite (bv_vt x)" |
|
167 apply (induct x rule: inducts(10)) |
|
168 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
169 apply (simp_all add: fv_supp finite_supp) |
|
170 done |
|
171 |
|
172 lemma fin_bv: "finite (bv x)" |
|
173 apply (induct x rule: inducts(9)) |
|
174 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
175 apply (simp add: finb1 finb2 finb3) |
|
176 done |
|
177 |
|
178 lemma "bv x \<sharp>* fv_bv x" |
|
179 apply (induct x rule: inducts(9)) |
|
180 apply (tactic {* ALLGOALS (TRY o rtac @{thm TrueI}) *}) |
|
181 apply (simp) |
|
182 oops |
95 |
183 |
96 lemma |
184 lemma |
97 assumes a01: "\<And>b. P1 b KStar" |
185 assumes a01: "\<And>b. P1 b KStar" |
98 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
186 and a02: "\<And>tkind1 tkind2 b. \<lbrakk>\<And>c. P1 c tkind1; \<And>c. P1 c tkind2\<rbrakk> \<Longrightarrow> P1 b (KFun tkind1 tkind2)" |
99 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
187 and a03: "\<And>ty1 ty2 b. \<lbrakk>\<And>c. P3 c ty1; \<And>c. P3 c ty2\<rbrakk> \<Longrightarrow> P2 b (CKEq ty1 ty2)" |
150 \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)" |
238 \<Longrightarrow> P12 b (TVCKCons tvar ckind tvck_lst)" |
151 shows "P1 (a :: 'a :: pt) tkind \<and> |
239 shows "P1 (a :: 'a :: pt) tkind \<and> |
152 P2 (b :: 'b :: pt) ckind \<and> |
240 P2 (b :: 'b :: pt) ckind \<and> |
153 P3 (c :: 'c :: {pt,fs}) ty \<and> |
241 P3 (c :: 'c :: {pt,fs}) ty \<and> |
154 P4 (d :: 'd :: pt) ty_lst \<and> |
242 P4 (d :: 'd :: pt) ty_lst \<and> |
155 P5 (e :: 'e :: pt) co \<and> |
243 P5 (e :: 'e :: {pt,fs}) co \<and> |
156 P6 (f :: 'f :: pt) co_lst \<and> |
244 P6 (f :: 'f :: pt) co_lst \<and> |
157 P7 (g :: 'g :: pt) trm \<and> |
245 P7 (g :: 'g :: pt) trm \<and> |
158 P8 (h :: 'h :: pt) assoc_lst \<and> |
246 P8 (h :: 'h :: {pt,fs}) assoc_lst \<and> |
159 P9 (i :: 'i :: pt) pat \<and> |
247 P9 (i :: 'i :: pt) pat \<and> |
160 P10 (j :: 'j :: pt) vt_lst \<and> |
248 P10 (j :: 'j :: pt) vt_lst \<and> |
161 P11 (k :: 'k :: pt) tvtk_lst \<and> |
249 P11 (k :: 'k :: pt) tvtk_lst \<and> |
162 P12 (l :: 'l :: pt) tvck_lst" |
250 P12 (l :: 'l :: pt) tvck_lst" |
163 proof - |
251 proof - |
164 have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
252 have a: "(\<forall>p a. P1 a (p \<bullet> tkind)) \<and> (\<forall>p b. P2 b (p \<bullet> ckind)) \<and> (\<forall>p c. P3 c (p \<bullet> ty)) \<and> (\<forall>p d. P4 d (p \<bullet> ty_lst)) \<and> (\<forall>p e. P5 e (p \<bullet> co)) \<and> (\<forall>p f. P6 f (p \<bullet> co_lst)) \<and> (\<forall>p g. P7 g (p \<bullet> trm)) \<and> (\<forall>p h. P8 h (p \<bullet> assoc_lst)) \<and> (\<forall>p i. P9 i (p \<bullet> pat)) \<and> (\<forall>p j. P10 j (p \<bullet> vt_lst)) \<and> (\<forall>p k. P11 k (p \<bullet> tvtk_lst)) \<and> (\<forall>p l. P12 l (p \<bullet> tvck_lst))" |
165 apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
253 apply (rule tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.induct) |
166 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
254 apply (tactic {* ALLGOALS (REPEAT o rtac allI) *}) |
167 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
255 apply (tactic {* ALLGOALS (TRY o SOLVED' (simp_tac @{simpset} THEN_ALL_NEW resolve_tac @{thms assms} THEN_ALL_NEW asm_full_simp_tac @{simpset})) *}) |
168 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
256 |
169 prefer 2 |
257 (* GOAL1 *) |
|
258 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> c \<and> |
|
259 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> ty)) \<sharp>* pa)") |
|
260 apply clarify |
|
261 apply (simp only: perm) |
|
262 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" |
|
263 and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
|
264 apply (simp only: eq_iff) |
|
265 apply (rule_tac x="-pa" in exI) |
|
266 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
|
267 apply (rule_tac t="supp (pa \<bullet> p \<bullet> ty) - {atom (pa \<bullet> p \<bullet> tvar)}" |
|
268 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
269 apply (simp add: eqvts) |
|
270 apply (simp add: eqvts[symmetric]) |
|
271 apply (rule conjI) |
|
272 apply (rule supp_perm_eq) |
|
273 apply (simp add: eqvts) |
|
274 apply (subst supp_finite_atom_set) |
|
275 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
276 apply (simp add: eqvts) |
|
277 apply (simp add: eqvts) |
|
278 apply (subst supp_perm_eq) |
|
279 apply (subst supp_finite_atom_set) |
|
280 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
281 apply (simp add: eqvts) |
|
282 apply assumption |
|
283 apply (simp add: fresh_star_minus_perm) |
|
284 apply (rule a08) |
|
285 apply simp |
|
286 apply(rotate_tac 1) |
|
287 apply(erule_tac x="(pa + p)" in allE) |
|
288 apply simp |
|
289 apply (simp add: eqvts eqvts_raw) |
170 apply (rule at_set_avoiding2_atom) |
290 apply (rule at_set_avoiding2_atom) |
171 apply (simp add: finite_supp) |
291 apply (simp add: finite_supp) |
172 apply (simp add: finite_supp) |
292 apply (simp add: finite_supp) |
173 apply (simp add: fresh_def) |
293 apply (simp add: fresh_def) |
174 apply (simp only: supp_Abs eqvts) |
294 apply (simp only: supp_Abs eqvts) |
175 apply blast |
295 apply blast |
|
296 |
|
297 (* GOAL2 *) |
|
298 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (atom (p \<bullet> tvar))) \<sharp> e \<and> |
|
299 supp (Abs (p \<bullet> {atom tvar}) (p \<bullet> co)) \<sharp>* pa)") |
176 apply clarify |
300 apply clarify |
177 apply (simp only: perm) |
301 apply (simp only: perm) |
178 apply(rule_tac t="TAll (p \<bullet> tvar) (p \<bullet> tkind) (p \<bullet> ty)" and s="TAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> tkind) (pa \<bullet> p \<bullet> ty)" in subst) |
302 apply(rule_tac t="CAll (p \<bullet> tvar) (p \<bullet> ckind) (p \<bullet> co)" |
179 apply (simp only: tkind_ckind_ty_ty_lst_co_co_lst_trm_assoc_lst_pat_vt_lst_tvtk_lst_tvck_lst.eq_iff) |
303 and s="CAll (pa \<bullet> p \<bullet> tvar) (p \<bullet> ckind) (pa \<bullet> p \<bullet> co)" in subst) |
|
304 apply (simp only: eq_iff) |
180 apply (rule_tac x="-pa" in exI) |
305 apply (rule_tac x="-pa" in exI) |
181 apply (simp add: alphas) |
306 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
182 prefer 2 |
307 apply (rule_tac t="supp (pa \<bullet> p \<bullet> co) - {atom (pa \<bullet> p \<bullet> tvar)}" |
183 apply (rule a08) |
308 and s="pa \<bullet> (p \<bullet> supp co - {p \<bullet> atom tvar})" in subst) |
|
309 apply (simp add: eqvts) |
|
310 apply (simp add: eqvts[symmetric]) |
|
311 apply (rule conjI) |
|
312 apply (rule supp_perm_eq) |
|
313 apply (simp add: eqvts) |
|
314 apply (subst supp_finite_atom_set) |
|
315 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
316 apply (simp add: eqvts) |
|
317 apply (simp add: eqvts) |
|
318 apply (subst supp_perm_eq) |
|
319 apply (subst supp_finite_atom_set) |
|
320 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
321 apply (simp add: eqvts) |
|
322 apply assumption |
|
323 apply (simp add: fresh_star_minus_perm) |
|
324 apply (rule a15) |
184 apply simp |
325 apply simp |
185 apply(rotate_tac 1) |
326 apply(rotate_tac 1) |
186 apply(erule_tac x="(pa + p)" in allE) |
327 apply(erule_tac x="(pa + p)" in allE) |
187 apply simp |
328 apply simp |
188 apply (simp add: eqvts eqvts_raw) |
329 apply (simp add: eqvts eqvts_raw) |
189 apply (simp add: eqvts eqvts_raw supp_Abs) |
330 apply (rule at_set_avoiding2_atom) |
|
331 apply (simp add: finite_supp) |
|
332 apply (simp add: finite_supp) |
|
333 apply (simp add: fresh_def) |
|
334 apply (simp only: supp_Abs eqvts) |
|
335 apply blast |
|
336 |
|
337 prefer 5 |
|
338 (* using a38*) |
|
339 apply(subgoal_tac "\<exists>pa. ((pa \<bullet> (bv (p \<bullet> pat))) \<sharp>* h \<and> |
|
340 supp (Abs (p \<bullet> (bv pat)) (p \<bullet> trm), fv_bv (p \<bullet> pat)) \<sharp>* pa)") |
|
341 apply clarify |
|
342 apply (simp only: perm) |
|
343 apply(rule_tac t="ACons (p \<bullet> pat) (p \<bullet> trm) (p \<bullet> assoc_lst)" |
|
344 and s="ACons (pa \<bullet> p \<bullet> pat) (pa \<bullet> p \<bullet> trm) (p \<bullet> assoc_lst)" in subst) |
|
345 apply (simp only: eq_iff supp_Pair fresh_star_union) |
|
346 apply (erule conjE) |
|
347 apply (rule_tac x="-pa" in exI) |
|
348 apply (simp add: alphas eqvts eqvts_raw supp_Abs fv_supp) |
|
349 apply (rule_tac t="supp (pa \<bullet> p \<bullet> trm) - bv (pa \<bullet> p \<bullet> pat)" |
|
350 and s="pa \<bullet> (supp (p \<bullet> trm) - bv (p \<bullet> pat))" in subst) |
|
351 apply (simp add: eqvts) |
|
352 apply (rule conjI) |
|
353 apply (rule fv_alpha) |
|
354 apply (rule_tac s="supp (fv_bv (p \<bullet> pat))" |
|
355 and t="fv_bv (p \<bullet> pat)" in subst) |
|
356 apply (rule supp_finite_atom_set[OF fin_fv_bv]) |
|
357 apply (assumption) |
190 apply (rule conjI) |
358 apply (rule conjI) |
191 apply (simp add: eqvts[symmetric]) |
359 apply (simp add: eqvts[symmetric]) |
192 apply (simp add: fv_supp) |
|
193 apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}" |
|
194 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
195 apply (simp add: eqvts) |
|
196 apply (rule supp_perm_eq) |
360 apply (rule supp_perm_eq) |
197 apply (simp add: eqvts) |
361 apply (simp add: eqvts) |
198 apply (subst supp_finite_atom_set) |
362 apply (subst supp_finite_atom_set) |
199 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
363 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
200 apply (simp add: eqvts) |
364 apply (simp add: eqvts) |
201 apply (simp add: eqvts) |
|
202 apply (simp add: fv_supp) |
|
203 apply (simp add: eqvts[symmetric]) |
|
204 apply (rule_tac t="pa \<bullet> p \<bullet> supp ty - {pa \<bullet> p \<bullet> atom tvar}" |
|
205 and s="pa \<bullet> (p \<bullet> supp ty - {p \<bullet> atom tvar})" in subst) |
|
206 apply (simp add: eqvts) |
365 apply (simp add: eqvts) |
207 apply (subst supp_perm_eq) |
366 apply (subst supp_perm_eq) |
208 apply (subst supp_finite_atom_set) |
367 apply (subst supp_finite_atom_set) |
209 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
368 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
210 apply (simp add: eqvts) |
369 apply (simp add: eqvts) |
211 apply assumption |
370 apply assumption |
212 apply (simp add: fresh_star_minus_perm) |
371 apply (simp add: fresh_star_minus_perm) |
|
372 apply (rule a38) |
|
373 apply(erule_tac x="(pa + p)" in allE) |
|
374 apply simp |
|
375 apply(rotate_tac 1) |
|
376 apply(erule_tac x="(pa + p)" in allE) |
|
377 apply simp |
|
378 apply simp |
|
379 apply (simp add: eqvts eqvts_raw) |
|
380 apply (rule at_set_avoiding2) |
|
381 apply (simp add: fin_bv) |
|
382 apply (simp add: finite_supp) |
|
383 apply (simp add: supp_Pair supp_Abs supp_finite_atom_set[OF fin_fv_bv] fin_fv_bv) |
|
384 apply (rule finite_Diff) |
|
385 apply (simp add: eqvts[symmetric] finite_eqvt[symmetric] finite_supp) |
|
386 apply (simp add: True_eqvt) |
|
387 apply (simp add: fresh_star_prod eqvts[symmetric]) |
|
388 apply (rule conjI) |
|
389 apply (simp add: fresh_star_def fresh_def supp_Abs) |
|
390 apply (simp add: fresh_star_permute_iff) |
213 sorry |
391 sorry |
214 |
|
215 have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
392 have g1: "P1 a (0 \<bullet> tkind)" using a[THEN conjunct1] by blast |
216 have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
393 have g2: "P2 b (0 \<bullet> ckind)" using a[THEN conjunct2,THEN conjunct1] by blast |
217 have g3: "P3 c (0 \<bullet> ty) \<and> |
394 have g3: "P3 c (0 \<bullet> ty) \<and> |
218 P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
395 P4 d (0 \<bullet> ty_lst) \<and> P5 e (0 \<bullet> co) \<and> P6 f (0 \<bullet> co_lst) \<and> |
219 P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |
396 P7 g (0 \<bullet> trm) \<and> P8 h (0 \<bullet> assoc_lst) \<and> P9 i (0 \<bullet> pat) \<and> |