milestone update in basic_2, update in ground and static_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpm_conf.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
index 141a733c230dfeccae7c25855b1db83223dcde17..3ef5de466273fa4774a2cfdf073373ed2302fd6d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/arith_2b.ma".
+include "ground/lib/arith_2b.ma".
 include "basic_2/rt_transition/lpr_lpr.ma".
 include "basic_2/rt_computation/cpms_lsubr.ma".
 include "basic_2/rt_computation/cpms_cpms.ma".
@@ -24,22 +24,22 @@ include "basic_2/dynamic/cnv_preserve_sub.ma".
 (* Sub diamond propery with t-bound rt-transition for terms *****************)
 
 fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93ª{I} â\9e¡*[0,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93ª{I} â\9e¡*[O,h] T.
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93ª[I] â\9e¡*[h,0] T & â\9dªG,L2â\9d« â\8a¢ â\93ª[I] â\9e¡*[h,0] T.
 /2 width=3 by ex2_intro/ qed-.
 
 fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s):
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\8b\86s â\9e¡*[1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\8b\86(next h s) â\9e¡*[h] T.
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\8b\86s â\9e¡*[h,1] T & â\9dªG,L2â\9d« â\8a¢ â\8b\86(⫯[h]s) â\9e¡*[h,0] T.
 /3 width=3 by cpm_cpms, ex2_intro/ qed-.
 
-fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (G) (L) (i):
-     (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84â\8a¢#i![a,h] →
-     â\88\80K,V. â¬\87*[i]L ≘ K.ⓓV →
-     â\88\80n,XV. â¦\83G,Kâ¦\84 â\8a¢ V â\9e¡[n,h] XV →
-     â\88\80X. â¬\86*[↑i]XV ≘ X →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ #i â\9e¡*[n,h] T & â¦\83G,L2â¦\84 â\8a¢ X â\9e¡*[h] T.
-#a #h #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
+fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i):
+     (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d«â\8a¢#i![h,a] →
+     â\88\80K,V. â\87©[i]L ≘ K.ⓓV →
+     â\88\80n,XV. â\9dªG,Kâ\9d« â\8a¢ V â\9e¡[h,n] XV →
+     â\88\80X. â\87§[↑i]XV ≘ X →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[h,n] T & â\9dªG,L2â\9d« â\8a¢ X â\9e¡*[h,0] T.
+#h #a #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
 lapply (cnv_inv_lref_pair … HT … HLK) -HT #HV
 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct
@@ -53,15 +53,15 @@ elim (cpms_lifts_sn … HVX … HLK2 … HXV) -XV -HLK2 #XV #HVX #HXV
 /3 width=6 by cpms_delta_drops, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (G) (L) (i):
-     (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84â\8a¢#i![a,h] →
-     â\88\80K,W. â¬\87*[i]L ≘ K.ⓛW →
-     â\88\80n,XW. â¦\83G,Kâ¦\84 â\8a¢ W â\9e¡[n,h] XW →
-     â\88\80X. â¬\86*[↑i]XW ≘ X →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ #i â\9e¡*[â\86\91n,h] T & â¦\83G,L2â¦\84 â\8a¢ X â\9e¡*[h] T.
-#a #h #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
+fact cnv_cpm_conf_lpr_atom_ell_aux (h) (a) (G) (L) (i):
+     (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d«â\8a¢#i![h,a] →
+     â\88\80K,W. â\87©[i]L ≘ K.ⓛW →
+     â\88\80n,XW. â\9dªG,Kâ\9d« â\8a¢ W â\9e¡[h,n] XW →
+     â\88\80X. â\87§[↑i]XW ≘ X →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ #i â\9e¡*[h,â\86\91n] T & â\9dªG,L2â\9d« â\8a¢ X â\9e¡*[h,0] T.
+#h #a #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
 lapply (cnv_inv_lref_pair … HT … HLK) -HT #HW
 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct
@@ -75,15 +75,15 @@ elim (cpms_lifts_sn … HWX … HLK2 … HXW) -XW -HLK2 #XW #HWX #HXW
 /3 width=6 by cpms_ell_drops, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (I) (G) (L) (i):
-     (â\88\80G0,L0,T0. â¦\83G,L,#iâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84â\8a¢#i![a,h] →
-     â\88\80K1,V1. â¬\87*[i]L â\89\98 K1.â\93\91{I}V1 â\86\92 â\88\80K2,V2. â¬\87*[i]L â\89\98 K2.â\93\91{I}V2 →
-     â\88\80n1,XV1. â¦\83G,K1â¦\84 â\8a¢ V1 â\9e¡[n1,h] XV1 â\86\92 â\88\80n2,XV2. â¦\83G,K2â¦\84 â\8a¢ V2 â\9e¡[n2,h] XV2 →
-     â\88\80X1. â¬\86*[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â¬\86*[↑i]XV2 ≘ X2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ X1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ X2 â\9e¡*[n1-n2,h] T.
-#a #h #I #G #L #i #IH #HT
+fact cnv_cpm_conf_lpr_delta_delta_aux (h) (a) (I) (G) (L) (i):
+     (â\88\80G0,L0,T0. â\9dªG,L,#iâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d«â\8a¢#i![h,a] →
+     â\88\80K1,V1. â\87©[i]L â\89\98 K1.â\93\91[I]V1 â\86\92 â\88\80K2,V2. â\87©[i]L â\89\98 K2.â\93\91[I]V2 →
+     â\88\80n1,XV1. â\9dªG,K1â\9d« â\8a¢ V1 â\9e¡[h,n1] XV1 â\86\92 â\88\80n2,XV2. â\9dªG,K2â\9d« â\8a¢ V2 â\9e¡[h,n2] XV2 →
+     â\88\80X1. â\87§[â\86\91i]XV1 â\89\98 X1 â\86\92 â\88\80X2. â\87§[↑i]XV2 ≘ X2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ X1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ X2 â\9e¡*[h,n1-n2] T.
+#h #a #I #G #L #i #IH #HT
 #K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2
 #L1 #HL1 #L2 #HL2
 lapply (drops_mono … HLY … HLK) -HLY #H destruct
@@ -102,41 +102,41 @@ elim (cpms_lifts_sn … HVX1 … HLK1 … HXV1) -XV1 -HLK1 #W1 #HVW1 #HXW1
 qed-.
 
 fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i):
-     â¬\87*[i]L â\89\98 K1.â\93\93V â\86\92 â¬\87*[i]L ≘ K2.ⓛW → ⊥.
+     â\87©[i]L â\89\98 K1.â\93\93V â\86\92 â\87©[i]L ≘ K2.ⓛW → ⊥.
 #L #K1 #K2 #V #W #i #HLK1 #HLK2
 lapply (drops_mono … HLK2 … HLK1) -L -i #H destruct
 qed-.
 
-fact cnv_cpm_conf_lpr_bind_bind_aux (a) (h) (p) (I) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\91{p,I}V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80n1,T1. â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\91{I}Vâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\91{p,I}V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\91{p,I}V2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #p #I #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_bind_bind_aux (h) (a) (p) (I) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\91[p,I]V.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\91[p,I]V.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80n1,T1. â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\91[I]Vâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\91[p,I]V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\91[p,I]V2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #p #I #G0 #L0 #V0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
-elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓑ[I]V1) … (L2.ⓑ[I]V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
 #T #HT1 #HT2 -L0 -V0 -T0
 /3 width=5 by cpms_bind_dx, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_bind_zeta_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,+â\93\93V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ +â\93\93V.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢V â\9e¡[h] V1 â\86\92 â\88\80n1,T1. â¦\83G,L.â\93\93Vâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 
-     â\88\80T2. â¬\86*[1]T2 â\89\98 T â\86\92 â\88\80n2,XT2. â¦\83G,Lâ¦\84 â\8a¢ T2 â\9e¡[n2,h] XT2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ +â\93\93V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ XT2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_bind_zeta_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ +â\93\93V.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢V â\9e¡[h,0] V1 â\86\92 â\88\80n1,T1. â\9dªG,L.â\93\93Vâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92
+     â\88\80T2. â\87§[1]T2 â\89\98 T â\86\92 â\88\80n2,XT2. â\9dªG,Lâ\9d« â\8a¢ T2 â\9e¡[h,n2] XT2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ +â\93\93V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ XT2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #V1 #HV01 #n1 #T1 #HT01 #T2 #HT20 #n2 #XT2 #HXT2
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_bind … H0) -H0 #_ #HT0
 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
-[ /3 width=3 by drops_refl, drops_drop/ ] #HT2 
+[ /3 width=3 by drops_refl, drops_drop/ ] #HT2
 elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01
 [| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12
 elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02)
@@ -144,14 +144,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02)
 /3 width=3 by cpms_zeta, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,+â\93\93V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ +â\93\93V.T ![a,h] →
-     â\88\80T1. â¬\86*[1]T1 â\89\98 T â\86\92 â\88\80T2. â¬\86*[1]T2 ≘ T →
-     â\88\80n1,XT1. â¦\83G,Lâ¦\84 â\8a¢ T1 â\9e¡[n1,h] XT1 â\86\92 â\88\80n2,XT2. â¦\83G,Lâ¦\84 â\8a¢ T2 â\9e¡[n2,h] XT2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ XT1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ XT2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,+â\93\93V.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ +â\93\93V.T ![h,a] →
+     â\88\80T1. â\87§[1]T1 â\89\98 T â\86\92 â\88\80T2. â\87§[1]T2 ≘ T →
+     â\88\80n1,XT1. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n1] XT1 â\86\92 â\88\80n2,XT2. â\9dªG,Lâ\9d« â\8a¢ T2 â\9e¡[h,n2] XT2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ XT1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ XT2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #T1 #HT10 #T2 #HT20 #n1 #XT1 #HXT1 #n2 #XT2 #HXT2
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_bind … H0) -H0 #_ #HT0
@@ -163,14 +163,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HXT1 … HXT2 … HL01 … HL02)
 /2 width=3 by ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_appl_appl_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\90V2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\90V2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
@@ -180,15 +180,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w
 /3 width=5 by cpms_appl_dx, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_appl_beta_aux (a) (h) (p) (G) (L) (V) (W) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\9b{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80W2. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W2 →
-     â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ â\93\9b{p}W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}â\93\9dW2.V2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80W2. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W2 →
+     â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\9b[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[p]â\93\9dW2.V2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
@@ -202,16 +202,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_
 /4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_appl_theta_aux (a) (h) (p) (G) (L) (V) (W) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\93{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\93{p}W.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80W2. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W2 →
-     â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ â\93\93{p}W.T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\93Wâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80U2. â¬\86*[1]V2 ≘ U2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\90V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}W2.â\93\90U2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\93[p]W.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80W2. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W2 →
+     â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ â\93\93[p]W.T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80U2. â\87§[1]V2 ≘ U2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\90V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[p]W2.â\93\90U2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #U2 #HVU2
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
@@ -225,7 +225,7 @@ elim (cpm_inv_abbr1 … HX) -HX *
   #T #HT1 #HT2 -L0 -V0 -W0 -T0
   /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/
 | #X0 #HXT0 #H1X0 #H destruct
-  lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0 
+  lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0
   elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
   elim (cnv_cpm_conf_lpr_sub … IH … H1X0 … HX02 … HL01 … HL02)
   [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0
@@ -233,15 +233,15 @@ elim (cpm_inv_abbr1 … HX) -HX *
 ]
 qed-.
 
-fact cnv_cpm_conf_lpr_beta_beta_aux (a) (h) (p) (G) (L) (V) (W) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\9b{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80W1. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W2 →
-     â\88\80n1,T1. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\93{p}â\93\9dW1.V1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}â\93\9dW2.V2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\9b[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W2 →
+     â\88\80n1,T1. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]â\93\9dW1.V1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[p]â\93\9dW2.V2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
@@ -255,16 +255,16 @@ lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_be
 /4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_theta_theta_aux (a) (h) (p) (G) (L) (V) (W) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\90V.â\93\93{p}W.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\93{p}W.T ![a,h] →
-     â\88\80V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V1 â\86\92 â\88\80V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[h] V2 →
-     â\88\80W1. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W1 â\86\92 â\88\80W2. â¦\83G,Lâ¦\84 â\8a¢ W â\9e¡[h] W2 →
-     â\88\80n1,T1. â¦\83G,L.â\93\93Wâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,L.â\93\93Wâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80U1. â¬\86*[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â¬\86*[1]V2 ≘ U2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\93{p}W1.â\93\90U1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\93{p}W2.â\93\90U2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #p #G0 #L0 #V0 #W0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\90V.â\93\93[p]W.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\93[p]W.T ![h,a] →
+     â\88\80V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V1 â\86\92 â\88\80V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,0] V2 →
+     â\88\80W1. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W1 â\86\92 â\88\80W2. â\9dªG,Lâ\9d« â\8a¢ W â\9e¡[h,0] W2 →
+     â\88\80n1,T1. â\9dªG,L.â\93\93Wâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,L.â\93\93Wâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80U1. â\87§[1]V1 â\89\98 U1 â\86\92 â\88\80U2. â\87§[1]V2 ≘ U2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\93[p]W2.â\93\90U2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #U1 #HVU1 #U2 #HVU2
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
@@ -278,14 +278,14 @@ lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3
 /4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_cast_cast_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n2,h] V2 →
-     â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ â\93\9dV2.T2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n2] V2 →
+     â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ â\93\9dV2.T2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
@@ -295,14 +295,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w
 /3 width=5 by cpms_cast, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_cast_epsilon_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 →
-     â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ T2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n1] V1 →
+     â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ T2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
@@ -311,15 +311,15 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w
 /3 width=3 by cpms_eps, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_cast_ee_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n2,h] V2 →
-     â\88\80T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ â\93\9dV1.T1 â\9e¡*[â\86\91n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ V2 â\9e¡*[n1-â\86\91n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n2] V2 →
+     â\88\80T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ â\93\9dV1.T1 â\9e¡*[h,â\86\91n2-n1] T & â\9dªG,L2â\9d« â\8a¢ V2 â\9e¡*[h,n1-â\86\91n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
 #L1 #HL01 #L2 #HL02 -HV01
 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
@@ -327,20 +327,20 @@ lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by f
 elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
-elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
 -L0 -V0 -T0 -X0 #U #HVU #HTU
 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
 lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
 /3 width=3 by cpms_eps, ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,T2. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n2,h] T2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ T1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ T2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,T2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n2] T2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ T2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #n1 #T1 #HT01 #n2 #T2 #HT02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0
@@ -349,14 +349,14 @@ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 w
 /2 width=3 by ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_epsilon_ee_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,T1. â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡[n1,h] T1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n2,h] V2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ T1 â\9e¡*[â\86\91n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ V2 â\9e¡*[n1-â\86\91n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
+fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,T1. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡[h,n1] T1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n2] V2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ T1 â\9e¡*[h,â\86\91n2-n1] T & â\9dªG,L2â\9d« â\8a¢ V2 â\9e¡*[h,n1-â\86\91n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
 #n1 #T1 #HT01 #n2 #V2 #HV02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
@@ -364,20 +364,20 @@ lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by f
 elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
-elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
+elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
 -L0 -V0 -T0 -X0 #U #HVU #HTU
 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
 lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
 /2 width=3 by ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_ee_ee_aux (a) (h) (G) (L) (V) (T):
-     (â\88\80G0,L0,T0. â¦\83G,L,â\93\9dV.Tâ¦\84 >[h] â¦\83G0,L0,T0â¦\84 â\86\92 IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
-     â¦\83G,Lâ¦\84 â\8a¢ â\93\9dV.T ![a,h] →
-     â\88\80n1,V1. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n1,h] V1 â\86\92 â\88\80n2,V2. â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡[n2,h] V2 →
-     â\88\80L1. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G,Lâ¦\84 â\8a¢ â\9e¡[h] L2 →
-     â\88\83â\88\83T. â¦\83G,L1â¦\84 â\8a¢ V1 â\9e¡*[n2-n1,h] T & â¦\83G,L2â¦\84 â\8a¢ V2 â\9e¡*[n1-n2,h] T.
-#a #h #G0 #L0 #V0 #T0 #IH #H0
+fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T):
+     (â\88\80G0,L0,T0. â\9dªG,L,â\93\9dV.Tâ\9d« > â\9dªG0,L0,T0â\9d« â\86\92 IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
+     â\9dªG,Lâ\9d« â\8a¢ â\93\9dV.T ![h,a] →
+     â\88\80n1,V1. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n1] V1 â\86\92 â\88\80n2,V2. â\9dªG,Lâ\9d« â\8a¢ V â\9e¡[h,n2] V2 →
+     â\88\80L1. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG,Lâ\9d« â\8a¢ â\9e¡[h,0] L2 →
+     â\88\83â\88\83T. â\9dªG,L1â\9d« â\8a¢ V1 â\9e¡*[h,n2-n1] T & â\9dªG,L2â\9d« â\8a¢ V2 â\9e¡*[h,n1-n2] T.
+#h #a #G0 #L0 #V0 #T0 #IH #H0
 #n1 #V1 #HV01 #n2 #V2 #HV02
 #L1 #HL01 #L2 #HL02
 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0
@@ -386,12 +386,12 @@ elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 w
 /2 width=3 by ex2_intro/
 qed-.
 
-fact cnv_cpm_conf_lpr_aux (a) (h):
-                          ∀G0,L0,T0.
-                          (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
-                          (∀G1,L1,T1. ⦃G0,L0,T0⦄ >[h] ⦃G1,L1,T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
-                          ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
-#a #h #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
+fact cnv_cpm_conf_lpr_aux (h) (a):
+     ∀G0,L0,T0.
+     (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
+     (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
+     ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr h a G1 L1 T1.
+#h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
 [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
   elim (cpm_inv_atom1_drops … HX1) -HX1 *
   elim (cpm_inv_atom1_drops … HX2) -HX2 *
@@ -423,7 +423,7 @@ fact cnv_cpm_conf_lpr_aux (a) (h):
     @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
   | #m2 #K2 #W2 #XW2 #i2 #HLK2 #_ #_ #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #_ #_ #H11 destruct -a -XW2 -XV1 -HL2 -HL1
     elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
-  | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2 
+  | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
     <minus_O_n <minus_n_O
     @ex2_commute @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
   | #s2 #H21 #H22 #H23 #m1 #K1 #W1 #XW1 #i1 #_ #_ #_ #H11 #H12 destruct