1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/rt_transition/lpr_lpr.ma".
16 include "basic_2/rt_computation/cpms_lsubr.ma".
17 include "basic_2/rt_computation/cpms_fpbg.ma".
18 include "basic_2/rt_computation/cpms_cpms.ma".
19 include "basic_2/dynamic/cnv_drops.ma".
20 include "basic_2/dynamic/cnv_preserve_far.ma".
22 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
24 (* Far diamond propery with t-bound rt-transition for terms *****************)
26 fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
27 ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡*[O,h] T.
28 /2 width=3 by ex2_intro/ qed-.
30 fact cnv_cpm_conf_lpr_atom_ess_aux (h) (G) (L1) (L2) (s):
31 ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡*[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡*[h] T.
32 /3 width=3 by cpm_cpms, ex2_intro/ qed-.
34 fact cnv_cpm_conf_lpr_atom_delta_aux (a) (h) (o) (G) (L) (i):
35 (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
38 ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
40 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
41 ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
42 #a #h #o #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
43 lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
44 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
45 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #HV1 #H destruct
46 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
47 elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
48 lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
49 lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
50 elim (cnv_cpm_conf_lpr_far … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
51 <minus_O_n <minus_n_O #V #HV1 #HVX
52 elim (cpms_lifts_sn … HVX … HLK2 … HXV) -XV -HLK2 #XV #HVX #HXV
53 /3 width=6 by cpms_delta_drops, ex2_intro/
56 fact cnv_cpm_conf_lpr_atom_ell_aux (a) (h) (o) (G) (L) (i):
57 (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
60 ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
62 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
63 ∃∃T. ⦃G,L1⦄ ⊢ #i ➡*[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡*[h] T.
64 #a #h #o #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
65 lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW
66 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
67 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #HK1 #HW1 #H destruct
68 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
69 elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct
70 lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
71 lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
72 elim (cnv_cpm_conf_lpr_far … IH … HW1 … HWX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
73 <minus_O_n <minus_n_O #W #HW1 #HWX
74 elim (cpms_lifts_sn … HWX … HLK2 … HXW) -XW -HLK2 #XW #HWX #HXW
75 /3 width=6 by cpms_ell_drops, ex2_intro/
78 fact cnv_cpm_conf_lpr_delta_delta_aux (a) (h) (o) (I) (G) (L) (i):
79 (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
81 ∀K1,V1. ⬇*[i]L ≘ K1.ⓑ{I}V1 → ∀K2,V2. ⬇*[i]L ≘ K2.ⓑ{I}V2 →
82 ∀n1,XV1. ⦃G,K1⦄ ⊢ V1 ➡[n1,h] XV1 → ∀n2,XV2. ⦃G,K2⦄ ⊢ V2 ➡[n2,h] XV2 →
83 ∀X1. ⬆*[↑i]XV1 ≘ X1 → ∀X2. ⬆*[↑i]XV2 ≘ X2 →
84 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
85 ∃∃T. ⦃G,L1⦄ ⊢ X1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ X2 ➡*[n1-n2,h] T.
86 #a #h #o #I #G #L #i #IH #HT
87 #K #V #HLK #Y #X #HLY #n1 #XV1 #HVX1 #n2 #XV2 #HVX2 #X1 #HXV1 #X2 #HXV2
89 lapply (drops_mono … HLY … HLK) -HLY #H destruct
90 lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
91 elim (lpr_drops_conf … HLK … HL1) -HL1 // #Y1 #H1 #HLK1
92 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #HK1 #_ #H destruct
93 lapply (drops_isuni_fwd_drop2 … HLK1) -V1 // #HLK1
94 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
95 elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
96 lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
97 lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
98 elim (cnv_cpm_conf_lpr_far … IH … HVX1 … HVX2 … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
100 elim (cpms_lifts_sn … HVX1 … HLK1 … HXV1) -XV1 -HLK1 #W1 #HVW1 #HXW1
101 /3 width=11 by cpms_lifts_bi, ex2_intro/
104 fact cnv_cpm_conf_lpr_delta_ell_aux (L) (K1) (K2) (V) (W) (i):
105 ⬇*[i]L ≘ K1.ⓓV → ⬇*[i]L ≘ K2.ⓛW → ⊥.
106 #L #K1 #K2 #V #W #i #HLK1 #HLK2
107 lapply (drops_mono … HLK2 … HLK1) -L -i #H destruct
110 fact cnv_cpm_conf_lpr_bind_bind_aux (a) (h) (o) (p) (I) (G) (L) (V) (T):
111 (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
112 ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] →
113 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
114 ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 →
115 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
116 ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡*[n1-n2,h] T.
117 #a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0
118 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
120 elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
121 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
122 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
123 #T #HT1 #HT2 -L0 -V0 -T0
124 /3 width=5 by cpms_bind_dx, ex2_intro/
127 fact cnv_cpm_conf_lpr_bind_zeta_aux (a) (h) (o) (G) (L) (V) (T):
128 (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
129 ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
130 ∀V1. ⦃G,L⦄ ⊢V ➡[h] V1 →
131 ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 →
132 ∀XT2. ⬆*[1]XT2 ≘ T2 →
133 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
134 ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
135 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
136 #V1 #HV01 #n1 #T1 #HT01 #n2 #T2 #HT02 #XT2 #HXT2
138 elim (cnv_inv_bind … H0) -H0 #_ #HT0
139 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0 -V0
141 elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 [| /3 width=1 by drops_refl, drops_drop/ ] #XT #HXT #HXT2
142 /3 width=3 by cpms_zeta, ex2_intro/
145 fact cnv_cpm_conf_lpr_zeta_zeta_aux (a) (h) (o) (G) (L) (V) (T):
146 (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
147 ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
148 ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓV⦄ ⊢ T ➡[n2,h] T2 →
149 ∀XT1. ⬆*[1]XT1 ≘ T1 → ∀XT2. ⬆*[1]XT2 ≘ T2 →
150 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
151 ∃∃T. ⦃G,L1⦄ ⊢ XT1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡*[n1-n2,h] T.
152 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
153 #n1 #T1 #HT01 #n2 #T2 #HT02 #XT1 #HXT1 #XT2 #HXT2
155 elim (cnv_inv_bind … H0) -H0 #_ #HT0
156 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ] -L0 -T0
158 elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #XT #HXT #HXT1
159 elim (cpms_inv_lifts_sn … HT2 (Ⓣ) … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #X #H #HXT2
160 lapply (lifts_inj … H … HXT) -T #H destruct
161 /2 width=3 by ex2_intro/
164 fact cnv_cpm_conf_lpr_appl_appl_aux (a) (h) (o) (G) (L) (V) (T):
165 (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
166 ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
167 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
168 ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
169 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
170 ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡*[n1-n2,h] T.
171 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
172 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
174 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
175 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
176 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
177 #T #HT1 #HT2 -L0 -V0 -T0
178 /3 width=5 by cpms_appl_dx, ex2_intro/
181 fact cnv_cpm_conf_lpr_appl_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
182 (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
183 ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
184 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
185 ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
186 ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
187 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
188 ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
189 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
190 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02
192 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
193 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
194 elim (cpm_inv_abst1 … HX) -HX #W1 #T1 #HW01 #HT01 #H destruct
195 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
196 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
197 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
198 #T #HT1 #HT2 -L0 -V0 -W0 -T0
199 lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_beta/ ] #HT2
200 /4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/
203 fact cnv_cpm_conf_lpr_appl_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
204 (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
205 ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
206 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
207 ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
208 ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
210 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
211 ∃∃T. ⦃G,L1⦄ ⊢ ⓐV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
212 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
213 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #U2 #HVU2
215 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
216 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
217 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
218 elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2
219 elim (cpm_inv_abbr1 … HX) -HX *
220 [ #W1 #T1 #HW01 #HT01 #H destruct
221 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
222 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
223 #T #HT1 #HT2 -L0 -V0 -W0 -T0
224 /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/
225 | #T1 #HT01 #HX #H destruct
226 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
227 #T #HT1 #HT2 -L0 -V0 -W0 -T0
228 elim (cpms_inv_lifts_sn … HT1 (Ⓣ) … L1 … HX) -T1 [| /3 width=1 by drops_refl, drops_drop/ ] #X0 #HXT #HX0
229 /4 width=7 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/
233 fact cnv_cpm_conf_lpr_beta_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
234 (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
235 ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
236 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
237 ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
238 ∀n1,T1. ⦃G,L.ⓛW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
239 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
240 ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}ⓝW1.V1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡*[n1-n2,h] T.
241 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
242 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02
244 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
245 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
246 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
247 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
248 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
249 #T #HT1 #HT2 -L0 -V0 -W0 -T0
250 lapply (lsubr_cpms_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ #HT1
251 lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ #HT2
252 /4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/
255 fact cnv_cpm_conf_lpr_theta_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
256 (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
257 ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
258 ∀V1. ⦃G,L⦄ ⊢ V ➡[h] V1 → ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
259 ∀W1. ⦃G,L⦄ ⊢ W ➡[h] W1 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
260 ∀n1,T1. ⦃G,L.ⓓW⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 →
261 ∀U1. ⬆*[1]V1 ≘ U1 → ∀U2. ⬆*[1]V2 ≘ U2 →
262 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
263 ∃∃T. ⦃G,L1⦄ ⊢ ⓓ{p}W1.ⓐU1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡*[n1-n2,h] T.
264 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
265 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #U1 #HVU1 #U2 #HVU2
267 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
268 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
269 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
270 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
271 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
272 #T #HT1 #HT2 -L0 -V0 -W0 -T0
273 elim (cpm_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
274 lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 width=1 by drops_refl, drops_drop/ ] #HU2
275 /4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/
278 fact cnv_cpm_conf_lpr_cast_cast_aux (a) (h) (o) (G) (L) (V) (T):
279 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
280 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
281 ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
282 ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
283 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
284 ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡*[n1-n2,h] T.
285 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
286 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02
288 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
289 elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
290 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
291 #T #HT1 #HT2 #V #HV1 #HV2 -L0 -V0 -T0
292 /3 width=5 by cpms_cast, ex2_intro/
295 fact cnv_cpm_conf_lpr_cast_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
296 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
297 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
298 ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 →
299 ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
300 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
301 ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
302 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
303 #n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
305 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
306 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
307 #T #HT1 #HT2 -L0 -V0 -T0
308 /3 width=3 by cpms_eps, ex2_intro/
311 fact cnv_cpm_conf_lpr_cast_ee_aux (a) (h) (o) (G) (L) (V) (T):
312 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
313 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
314 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
315 ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
316 ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 →
317 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
318 ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T.
319 #a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
320 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
321 #L1 #HL01 #L2 #HL02 -HV01
322 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
323 lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
324 elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
325 elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
326 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
327 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
328 -L0 -V0 -T0 -X0 #U #HVU #HTU
329 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
330 lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
331 /3 width=3 by cpms_eps, ex2_intro/
334 fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
335 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
336 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
337 ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
338 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
339 ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
340 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
341 #n1 #T1 #HT01 #n2 #T2 #HT02
343 elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0
344 elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
345 #T #HT1 #HT2 -L0 -V0 -T0
346 /2 width=3 by ex2_intro/
349 fact cnv_cpm_conf_lpr_epsilon_ee_aux (a) (h) (o) (G) (L) (V) (T):
350 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
351 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
352 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
353 ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
354 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
355 ∃∃T. ⦃G,L1⦄ ⊢ T1 ➡*[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-↑n2,h] T.
356 #a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
357 #n1 #T1 #HT01 #n2 #V2 #HV02
359 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
360 lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
361 elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
362 elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
363 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
364 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
365 -L0 -V0 -T0 -X0 #U #HVU #HTU
366 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
367 lapply (cpms_trans … HT1 … HTU) -T <arith_l #H1
368 /2 width=3 by ex2_intro/
371 fact cnv_cpm_conf_lpr_ee_ee_aux (a) (h) (o) (G) (L) (V) (T):
372 (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpms_conf_lpr a h G0 L0 T0) →
373 ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
374 ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
375 ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
376 ∃∃T. ⦃G,L1⦄ ⊢ V1 ➡*[n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡*[n1-n2,h] T.
377 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
378 #n1 #V1 #HV01 #n2 #V2 #HV02
380 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0
381 elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
382 #V #HV1 #HV2 -L0 -V0 -T0
383 /2 width=3 by ex2_intro/
386 fact cnv_cpm_conf_lpr_aux (a) (h) (o):
388 (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
389 (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
390 ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
391 #a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
392 [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
393 elim (cpm_inv_atom1_drops … HX1) -HX1 *
394 elim (cpm_inv_atom1_drops … HX2) -HX2 *
395 [ #H21 #H22 #H11 #H12 destruct -L -a -o
397 /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
398 | #s2 #H21 #H22 #H23 #H11 #H12 destruct -L -a -o
399 <minus_O_n <minus_n_O
400 /2 width=1 by cnv_cpm_conf_lpr_atom_ess_aux/
401 | #K2 #V2 #XV2 #i #HLK2 #HVX2 #HXV2 #H21 #H11 #H12 destruct -IH2
402 <minus_O_n <minus_n_O
403 @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
404 | #m2 #K2 #W2 #XW2 #i #HLK2 #HWX2 #HXW2 #H21 #H22 #H11 #H12 destruct -IH2
405 <minus_O_n <minus_n_O
406 @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
407 | #H21 #H22 #s1 #H11 #H12 #H13 destruct -L -a -o
408 <minus_O_n <minus_n_O
409 /3 width=1 by cnv_cpm_conf_lpr_atom_ess_aux, ex2_commute/
410 | #s2 #H21 #H22 #H23 #s1 #H11 #H12 #H13 destruct -L -a -o
412 /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
413 | #K2 #V2 #XV2 #i2 #_ #_ #_ #H21 #s1 #H11 #H12 #H13 destruct
414 | #m2 #K2 #W2 #XW2 #i2 #_ #_ #_ #H21 #H22 #s1 #H11 #H12 #H13 destruct
415 | #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
416 <minus_O_n <minus_n_O
417 @ex2_commute @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
418 | #s2 #H21 #H22 #H23 #K1 #V1 #XV1 #i1 #_ #_ #_ #H11 destruct
419 | #K2 #V2 #XV2 #i2 #HLK2 #HVX2 #HXV2 #H21 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
420 @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
421 | #m2 #K2 #W2 #XW2 #i2 #HLK2 #_ #_ #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #_ #_ #H11 destruct -a -o -XW2 -XV1 -HL2 -HL1
422 elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
423 | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
424 <minus_O_n <minus_n_O
425 @ex2_commute @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
426 | #s2 #H21 #H22 #H23 #m1 #K1 #W1 #XW1 #i1 #_ #_ #_ #H11 #H12 destruct
427 | #K2 #V2 #XV2 #i2 #HLK2 #_ #_ #H21 #m1 #K1 #W1 #XW1 #i1 #HLK1 #_ #_ #H11 #H12 destruct -a -o -XV2 -XW1 -HL2 -HL1
428 elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
429 | #m2 #K2 #W2 #XW2 #i2 #HLK2 #HWX2 #HXW2 #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
430 >minus_S_S >minus_S_S
431 @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
433 | #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
434 elim (cpm_inv_bind1 … HX1) -HX1 *
435 elim (cpm_inv_bind1 … HX2) -HX2 *
436 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
437 @(cnv_cpm_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
438 | #T2 #HT2 #HXT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
439 @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
440 | #V2 #T2 #HV2 #HT2 #H21 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2
441 @ex2_commute @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
442 | #T2 #HT2 #HXT2 #H21 #H22 #T1 #HT1 #HXT1 #H11 #H12 destruct -IH2
443 @(cnv_cpm_conf_lpr_zeta_zeta_aux … IH1) -IH1 /1 width=3 by/
445 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
446 elim (cpm_inv_appl1 … HX1) -HX1 *
447 elim (cpm_inv_appl1 … HX2) -HX2 *
448 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
449 @(cnv_cpm_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
450 | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
451 @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
452 | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
453 @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
454 | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
455 @ex2_commute @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
456 | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
457 @(cnv_cpm_conf_lpr_beta_beta_aux … IH1) -IH1 /1 width=1 by/
458 | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct
459 | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct -IH2
460 @ex2_commute @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
461 | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct
462 | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct -IH2
463 @(cnv_cpm_conf_lpr_theta_theta_aux … IH1) -IH1 /1 width=3 by/
465 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
466 elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
467 elim (cpm_inv_cast1 … HX2) -HX2 [ * || * | * || * | * || * ]
468 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
469 @(cnv_cpm_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
470 | #HT2 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
471 @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
472 | #m2 #HV2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct
473 @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
474 | #V2 #T2 #HV2 #HT2 #H21 #HT1 destruct -IH2
475 @ex2_commute @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
477 @(cnv_cpm_conf_lpr_epsilon_epsilon_aux … IH1) -IH1 /1 width=1 by/
478 | #m2 #HV2 #H21 #HT1 destruct
479 @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
480 | #V2 #T2 #HV2 #HT2 #H21 #m1 #HV1 #H11 destruct
481 @ex2_commute @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
482 | #HT2 #m1 #HV1 #H11 destruct
483 @ex2_commute @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
484 | #m2 #HV2 #H21 #m1 #HV1 #H11 destruct -IH2
485 >minus_S_S >minus_S_S
486 @(cnv_cpm_conf_lpr_ee_ee_aux … IH1) -IH1 /1 width=1 by/