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 "ground/lib/arith_2b.ma".
16 include "basic_2/rt_transition/lpr_lpr.ma".
17 include "basic_2/rt_computation/cpms_lsubr.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_sub.ma".
22 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
24 (* Sub 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] ➡*[h,0] T & ❨G,L2❩ ⊢ ⓪[I] ➡*[h,0] 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 ➡*[h,1] T & ❨G,L2❩ ⊢ ⋆(⫯[h]s) ➡*[h,0] T.
32 /3 width=3 by cpm_cpms, ex2_intro/ qed-.
34 fact cnv_cpm_conf_lpr_atom_delta_aux (h) (a) (G) (L) (i):
35 (∀G0,L0,T0. ❨G,L,#i❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
38 ∀n,XV. ❨G,K❩ ⊢ V ➡[h,n] XV →
40 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
41 ∃∃T. ❨G,L1❩ ⊢ #i ➡*[h,n] T & ❨G,L2❩ ⊢ X ➡*[h,0] T.
42 #h #a #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #HL1 #L2 #HL2
43 lapply (cnv_inv_lref_pair … 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_sub … 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 (h) (a) (G) (L) (i):
57 (∀G0,L0,T0. ❨G,L,#i❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
60 ∀n,XW. ❨G,K❩ ⊢ W ➡[h,n] XW →
62 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
63 ∃∃T. ❨G,L1❩ ⊢ #i ➡*[h,↑n] T & ❨G,L2❩ ⊢ X ➡*[h,0] T.
64 #h #a #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #HL1 #L2 #HL2
65 lapply (cnv_inv_lref_pair … 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_sub … 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 (h) (a) (I) (G) (L) (i):
79 (∀G0,L0,T0. ❨G,L,#i❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
81 ∀K1,V1. ⇩[i]L ≘ K1.ⓑ[I]V1 → ∀K2,V2. ⇩[i]L ≘ K2.ⓑ[I]V2 →
82 ∀n1,XV1. ❨G,K1❩ ⊢ V1 ➡[h,n1] XV1 → ∀n2,XV2. ❨G,K2❩ ⊢ V2 ➡[h,n2] XV2 →
83 ∀X1. ⇧[↑i]XV1 ≘ X1 → ∀X2. ⇧[↑i]XV2 ≘ X2 →
84 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
85 ∃∃T. ❨G,L1❩ ⊢ X1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ X2 ➡*[h,n1-n2] T.
86 #h #a #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_inv_lref_pair … 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_sub … 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 (h) (a) (p) (I) (G) (L) (V) (T):
111 (∀G0,L0,T0. ❨G,L,ⓑ[p,I]V.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
112 ❨G,L❩ ⊢ ⓑ[p,I]V.T ![h,a] →
113 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
114 ∀n1,T1. ❨G,L.ⓑ[I]V❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L.ⓑ[I]V❩ ⊢ T ➡[h,n2] T2 →
115 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
116 ∃∃T. ❨G,L1❩ ⊢ ⓑ[p,I]V1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓑ[p,I]V2.T2 ➡*[h,n1-n2] T.
117 #h #a #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_sub … 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 (h) (a) (G) (L) (V) (T):
128 (∀G0,L0,T0. ❨G,L,+ⓓV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
129 ❨G,L❩ ⊢ +ⓓV.T ![h,a] →
130 ∀V1. ❨G,L❩ ⊢V ➡[h,0] V1 → ∀n1,T1. ❨G,L.ⓓV❩ ⊢ T ➡[h,n1] T1 →
131 ∀T2. ⇧[1]T2 ≘ T → ∀n2,XT2. ❨G,L❩ ⊢ T2 ➡[h,n2] XT2 →
132 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
133 ∃∃T. ❨G,L1❩ ⊢ +ⓓV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ XT2 ➡*[h,n1-n2] T.
134 #h #a #G0 #L0 #V0 #T0 #IH #H0
135 #V1 #HV01 #n1 #T1 #HT01 #T2 #HT20 #n2 #XT2 #HXT2
137 elim (cnv_inv_bind … H0) -H0 #_ #HT0
138 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
139 [ /3 width=3 by drops_refl, drops_drop/ ] #HT2
140 elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01
141 [| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12
142 elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02)
143 [|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 -V0 #T #HT1 #HT2
144 /3 width=3 by cpms_zeta, ex2_intro/
147 fact cnv_cpm_conf_lpr_zeta_zeta_aux (h) (a) (G) (L) (V) (T):
148 (∀G0,L0,T0. ❨G,L,+ⓓV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
149 ❨G,L❩ ⊢ +ⓓV.T ![h,a] →
150 ∀T1. ⇧[1]T1 ≘ T → ∀T2. ⇧[1]T2 ≘ T →
151 ∀n1,XT1. ❨G,L❩ ⊢ T1 ➡[h,n1] XT1 → ∀n2,XT2. ❨G,L❩ ⊢ T2 ➡[h,n2] XT2 →
152 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
153 ∃∃T. ❨G,L1❩ ⊢ XT1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ XT2 ➡*[h,n1-n2] T.
154 #h #a #G0 #L0 #V0 #T0 #IH #H0
155 #T1 #HT10 #T2 #HT20 #n1 #XT1 #HXT1 #n2 #XT2 #HXT2
157 elim (cnv_inv_bind … H0) -H0 #_ #HT0
158 lapply (lifts_inj … HT10 … HT20) -HT10 #H destruct
159 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
160 [ /3 width=3 by drops_refl, drops_drop/ ] #HT2
161 elim (cnv_cpm_conf_lpr_sub … IH … HXT1 … HXT2 … HL01 … HL02)
162 [|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #HT2
163 /2 width=3 by ex2_intro/
166 fact cnv_cpm_conf_lpr_appl_appl_aux (h) (a) (G) (L) (V) (T):
167 (∀G0,L0,T0. ❨G,L,ⓐV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
168 ❨G,L❩ ⊢ ⓐV.T ![h,a] →
169 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
170 ∀n1,T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L❩ ⊢ T ➡[h,n2] T2 →
171 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
172 ∃∃T. ❨G,L1❩ ⊢ ⓐV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓐV2.T2 ➡*[h,n1-n2] T.
173 #h #a #G0 #L0 #V0 #T0 #IH #H0
174 #V1 #HV01 #V2 #HV02 #n1 #T1 #HT01 #n2 #T2 #HT02
176 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
177 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
178 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
179 #T #HT1 #HT2 -L0 -V0 -T0
180 /3 width=5 by cpms_appl_dx, ex2_intro/
183 fact cnv_cpm_conf_lpr_appl_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
184 (∀G0,L0,T0. ❨G,L,ⓐV.ⓛ[p]W.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
185 ❨G,L❩ ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
186 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
187 ∀W2. ❨G,L❩ ⊢ W ➡[h,0] W2 →
188 ∀n1,T1. ❨G,L❩ ⊢ ⓛ[p]W.T ➡[h,n1] T1 → ∀n2,T2. ❨G,L.ⓛW❩ ⊢ T ➡[h,n2] T2 →
189 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
190 ∃∃T. ❨G,L1❩ ⊢ ⓐV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
191 #h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
192 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02
194 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
195 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
196 elim (cpm_inv_abst1 … HX) -HX #W1 #T1 #HW01 #HT01 #H destruct
197 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
198 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
199 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
200 #T #HT1 #HT2 -L0 -V0 -W0 -T0
201 lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_beta/ ] #HT2
202 /4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/
205 fact cnv_cpm_conf_lpr_appl_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
206 (∀G0,L0,T0. ❨G,L,ⓐV.ⓓ[p]W.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
207 ❨G,L❩ ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
208 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
209 ∀W2. ❨G,L❩ ⊢ W ➡[h,0] W2 →
210 ∀n1,T1. ❨G,L❩ ⊢ ⓓ[p]W.T ➡[h,n1] T1 → ∀n2,T2. ❨G,L.ⓓW❩ ⊢ T ➡[h,n2] T2 →
212 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
213 ∃∃T. ❨G,L1❩ ⊢ ⓐV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
214 #h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
215 #V1 #HV01 #V2 #HV02 #W2 #HW02 #n1 #X #HX #n2 #T2 #HT02 #U2 #HVU2
217 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
218 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
219 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
220 elim (cpm_inv_abbr1 … HX) -HX *
221 [ #W1 #T1 #HW01 #HT01 #H destruct
222 elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HV2 -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2
223 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
224 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
225 #T #HT1 #HT2 -L0 -V0 -W0 -T0
226 /4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/
227 | #X0 #HXT0 #H1X0 #H destruct
228 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0
229 elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
230 elim (cnv_cpm_conf_lpr_sub … IH … H1X0 … HX02 … HL01 … HL02)
231 [|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0
232 /4 width=8 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/
236 fact cnv_cpm_conf_lpr_beta_beta_aux (h) (a) (p) (G) (L) (V) (W) (T):
237 (∀G0,L0,T0. ❨G,L,ⓐV.ⓛ[p]W.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
238 ❨G,L❩ ⊢ ⓐV.ⓛ[p]W.T ![h,a] →
239 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
240 ∀W1. ❨G,L❩ ⊢ W ➡[h,0] W1 → ∀W2. ❨G,L❩ ⊢ W ➡[h,0] W2 →
241 ∀n1,T1. ❨G,L.ⓛW❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L.ⓛW❩ ⊢ T ➡[h,n2] T2 →
242 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
243 ∃∃T. ❨G,L1❩ ⊢ ⓓ[p]ⓝW1.V1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓓ[p]ⓝW2.V2.T2 ➡*[h,n1-n2] T.
244 #h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
245 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02
247 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
248 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
249 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
250 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
251 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
252 #T #HT1 #HT2 -L0 -V0 -W0 -T0
253 lapply (lsubr_cpms_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ #HT1
254 lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ #HT2
255 /4 width=5 by cpms_bind_dx, cpm_eps, ex2_intro/
258 fact cnv_cpm_conf_lpr_theta_theta_aux (h) (a) (p) (G) (L) (V) (W) (T):
259 (∀G0,L0,T0. ❨G,L,ⓐV.ⓓ[p]W.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
260 ❨G,L❩ ⊢ ⓐV.ⓓ[p]W.T ![h,a] →
261 ∀V1. ❨G,L❩ ⊢ V ➡[h,0] V1 → ∀V2. ❨G,L❩ ⊢ V ➡[h,0] V2 →
262 ∀W1. ❨G,L❩ ⊢ W ➡[h,0] W1 → ∀W2. ❨G,L❩ ⊢ W ➡[h,0] W2 →
263 ∀n1,T1. ❨G,L.ⓓW❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L.ⓓW❩ ⊢ T ➡[h,n2] T2 →
264 ∀U1. ⇧[1]V1 ≘ U1 → ∀U2. ⇧[1]V2 ≘ U2 →
265 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
266 ∃∃T. ❨G,L1❩ ⊢ ⓓ[p]W1.ⓐU1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓓ[p]W2.ⓐU2.T2 ➡*[h,n1-n2] T.
267 #h #a #p #G0 #L0 #V0 #W0 #T0 #IH #H0
268 #V1 #HV01 #V2 #HV02 #W1 #HW01 #W2 #HW02 #n1 #T1 #HT01 #n2 #T2 #HT02 #U1 #HVU1 #U2 #HVU2
270 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
271 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
272 elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
273 elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
274 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
275 #T #HT1 #HT2 -L0 -V0 -W0 -T0
276 elim (cpm_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
277 lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 width=1 by drops_refl, drops_drop/ ] #HU2
278 /4 width=7 by cpms_appl_dx, cpms_bind_dx, ex2_intro/
281 fact cnv_cpm_conf_lpr_cast_cast_aux (h) (a) (G) (L) (V) (T):
282 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
283 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
284 ∀n1,V1. ❨G,L❩ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❨G,L❩ ⊢ V ➡[h,n2] V2 →
285 ∀T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 → ∀T2. ❨G,L❩ ⊢ T ➡[h,n2] T2 →
286 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
287 ∃∃T. ❨G,L1❩ ⊢ ⓝV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ ⓝV2.T2 ➡*[h,n1-n2] T.
288 #h #a #G0 #L0 #V0 #T0 #IH #H0
289 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02
291 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
292 elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
293 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
294 #T #HT1 #HT2 #V #HV1 #HV2 -L0 -V0 -T0
295 /3 width=5 by cpms_cast, ex2_intro/
298 fact cnv_cpm_conf_lpr_cast_epsilon_aux (h) (a) (G) (L) (V) (T):
299 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
300 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
301 ∀n1,V1. ❨G,L❩ ⊢ V ➡[h,n1] V1 →
302 ∀T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L❩ ⊢ T ➡[h,n2] T2 →
303 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
304 ∃∃T. ❨G,L1❩ ⊢ ⓝV1.T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ T2 ➡*[h,n1-n2] T.
305 #h #a #G0 #L0 #V0 #T0 #IH #H0
306 #n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
308 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
309 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
310 #T #HT1 #HT2 -L0 -V0 -T0
311 /3 width=3 by cpms_eps, ex2_intro/
314 fact cnv_cpm_conf_lpr_cast_ee_aux (h) (a) (G) (L) (V) (T):
315 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
316 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
317 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
318 ∀n1,V1. ❨G,L❩ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❨G,L❩ ⊢ V ➡[h,n2] V2 →
319 ∀T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 →
320 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
321 ∃∃T. ❨G,L1❩ ⊢ ⓝV1.T1 ➡*[h,↑n2-n1] T & ❨G,L2❩ ⊢ V2 ➡*[h,n1-↑n2] T.
322 #h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
323 #n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
324 #L1 #HL01 #L2 #HL02 -HV01
325 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
326 lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
327 elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
328 elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
329 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
330 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
331 -L0 -V0 -T0 -X0 #U #HVU #HTU
332 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
333 lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
334 /3 width=3 by cpms_eps, ex2_intro/
337 fact cnv_cpm_conf_lpr_epsilon_epsilon_aux (h) (a) (G) (L) (V) (T):
338 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
339 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
340 ∀n1,T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 → ∀n2,T2. ❨G,L❩ ⊢ T ➡[h,n2] T2 →
341 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
342 ∃∃T. ❨G,L1❩ ⊢ T1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ T2 ➡*[h,n1-n2] T.
343 #h #a #G0 #L0 #V0 #T0 #IH #H0
344 #n1 #T1 #HT01 #n2 #T2 #HT02
346 elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0
347 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
348 #T #HT1 #HT2 -L0 -V0 -T0
349 /2 width=3 by ex2_intro/
352 fact cnv_cpm_conf_lpr_epsilon_ee_aux (h) (a) (G) (L) (V) (T):
353 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpm_trans_lpr h a G0 L0 T0) →
354 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
355 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
356 ∀n1,T1. ❨G,L❩ ⊢ T ➡[h,n1] T1 → ∀n2,V2. ❨G,L❩ ⊢ V ➡[h,n2] V2 →
357 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
358 ∃∃T. ❨G,L1❩ ⊢ T1 ➡*[h,↑n2-n1] T & ❨G,L2❩ ⊢ V2 ➡*[h,n1-↑n2] T.
359 #h #a #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
360 #n1 #T1 #HT01 #n2 #V2 #HV02
362 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
363 lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
364 elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
365 elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
366 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
367 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=5 by fqup_cpms_fwd_fpbg/ ]
368 -L0 -V0 -T0 -X0 #U #HVU #HTU
369 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
370 lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
371 /2 width=3 by ex2_intro/
374 fact cnv_cpm_conf_lpr_ee_ee_aux (h) (a) (G) (L) (V) (T):
375 (∀G0,L0,T0. ❨G,L,ⓝV.T❩ > ❨G0,L0,T0❩ → IH_cnv_cpms_conf_lpr h a G0 L0 T0) →
376 ❨G,L❩ ⊢ ⓝV.T ![h,a] →
377 ∀n1,V1. ❨G,L❩ ⊢ V ➡[h,n1] V1 → ∀n2,V2. ❨G,L❩ ⊢ V ➡[h,n2] V2 →
378 ∀L1. ❨G,L❩ ⊢ ➡[h,0] L1 → ∀L2. ❨G,L❩ ⊢ ➡[h,0] L2 →
379 ∃∃T. ❨G,L1❩ ⊢ V1 ➡*[h,n2-n1] T & ❨G,L2❩ ⊢ V2 ➡*[h,n1-n2] T.
380 #h #a #G0 #L0 #V0 #T0 #IH #H0
381 #n1 #V1 #HV01 #n2 #V2 #HV02
383 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0
384 elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
385 #V #HV1 #HV2 -L0 -V0 -T0
386 /2 width=3 by ex2_intro/
389 fact cnv_cpm_conf_lpr_aux (h) (a):
391 (∀G1,L1,T1. ❨G0,L0,T0❩ > ❨G1,L1,T1❩ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) →
392 (∀G1,L1,T1. ❨G0,L0,T0❩ > ❨G1,L1,T1❩ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) →
393 ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_conf_lpr h a G1 L1 T1.
394 #h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
395 [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
396 elim (cpm_inv_atom1_drops … HX1) -HX1 *
397 elim (cpm_inv_atom1_drops … HX2) -HX2 *
398 [ #H21 #H22 #H11 #H12 destruct -a -L
400 /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
401 | #s2 #H21 #H22 #H23 #H11 #H12 destruct -a -L
402 <minus_O_n <minus_n_O
403 /2 width=1 by cnv_cpm_conf_lpr_atom_ess_aux/
404 | #K2 #V2 #XV2 #i #HLK2 #HVX2 #HXV2 #H21 #H11 #H12 destruct -IH2
405 <minus_O_n <minus_n_O
406 @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
407 | #m2 #K2 #W2 #XW2 #i #HLK2 #HWX2 #HXW2 #H21 #H22 #H11 #H12 destruct -IH2
408 <minus_O_n <minus_n_O
409 @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
410 | #H21 #H22 #s1 #H11 #H12 #H13 destruct -a -L
411 <minus_O_n <minus_n_O
412 /3 width=1 by cnv_cpm_conf_lpr_atom_ess_aux, ex2_commute/
413 | #s2 #H21 #H22 #H23 #s1 #H11 #H12 #H13 destruct -a -L
415 /2 width=1 by cnv_cpm_conf_lpr_atom_atom_aux/
416 | #K2 #V2 #XV2 #i2 #_ #_ #_ #H21 #s1 #H11 #H12 #H13 destruct
417 | #m2 #K2 #W2 #XW2 #i2 #_ #_ #_ #H21 #H22 #s1 #H11 #H12 #H13 destruct
418 | #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
419 <minus_O_n <minus_n_O
420 @ex2_commute @(cnv_cpm_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
421 | #s2 #H21 #H22 #H23 #K1 #V1 #XV1 #i1 #_ #_ #_ #H11 destruct
422 | #K2 #V2 #XV2 #i2 #HLK2 #HVX2 #HXV2 #H21 #K1 #V1 #XV1 #i1 #HLK1 #HVX1 #HXV1 #H11 destruct -IH2
423 @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
424 | #m2 #K2 #W2 #XW2 #i2 #HLK2 #_ #_ #H21 #H22 #K1 #V1 #XV1 #i1 #HLK1 #_ #_ #H11 destruct -a -XW2 -XV1 -HL2 -HL1
425 elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
426 | #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
427 <minus_O_n <minus_n_O
428 @ex2_commute @(cnv_cpm_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
429 | #s2 #H21 #H22 #H23 #m1 #K1 #W1 #XW1 #i1 #_ #_ #_ #H11 #H12 destruct
430 | #K2 #V2 #XV2 #i2 #HLK2 #_ #_ #H21 #m1 #K1 #W1 #XW1 #i1 #HLK1 #_ #_ #H11 #H12 destruct -a -XV2 -XW1 -HL2 -HL1
431 elim cnv_cpm_conf_lpr_delta_ell_aux /1 width=8 by/
432 | #m2 #K2 #W2 #XW2 #i2 #HLK2 #HWX2 #HXW2 #H21 #H22 #m1 #K1 #W1 #XW1 #i1 #HLK1 #HWX1 #HXW1 #H11 #H12 destruct -IH2
433 >minus_S_S >minus_S_S
434 @(cnv_cpm_conf_lpr_delta_delta_aux … IH1) -IH1 /1 width=13 by/
436 | #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
437 elim (cpm_inv_bind1 … HX1) -HX1 *
438 elim (cpm_inv_bind1 … HX2) -HX2 *
439 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
440 @(cnv_cpm_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
441 | #T2 #HT2 #HTX2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
442 @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
443 | #V2 #T2 #HV2 #HT2 #H21 #T1 #HT1 #HTX1 #H11 #H12 destruct -IH2
444 @ex2_commute @(cnv_cpm_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
445 | #T2 #HT2 #HTX2 #H21 #H22 #T1 #HT1 #HTX1 #H11 #H12 destruct -IH2
446 @(cnv_cpm_conf_lpr_zeta_zeta_aux … IH1) -IH1 /1 width=3 by/
448 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
449 elim (cpm_inv_appl1 … HX1) -HX1 *
450 elim (cpm_inv_appl1 … HX2) -HX2 *
451 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
452 @(cnv_cpm_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
453 | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
454 @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
455 | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
456 @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
457 | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
458 @ex2_commute @(cnv_cpm_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
459 | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #p1 #V1 #XW1 #W1 #XT1 #T1 #HV1 #HW1 #HT1 #H11 #H12 destruct -IH2
460 @(cnv_cpm_conf_lpr_beta_beta_aux … IH1) -IH1 /1 width=1 by/
461 | #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
462 | #V2 #T2 #HV2 #HT2 #H21 #p1 #V1 #XV1 #XW1 #W1 #XT1 #T1 #HV1 #HXV1 #HW1 #HT1 #H11 #H12 destruct -IH2
463 @ex2_commute @(cnv_cpm_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
464 | #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
465 | #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
466 @(cnv_cpm_conf_lpr_theta_theta_aux … IH1) -IH1 /1 width=3 by/
468 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #HX1 #n2 #X2 #HX2 #L1 #HL1 #L2 #HL2 destruct
469 elim (cpm_inv_cast1 … HX1) -HX1 [ * || * ]
470 elim (cpm_inv_cast1 … HX2) -HX2 [ * || * | * || * | * || * ]
471 [ #V2 #T2 #HV2 #HT2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
472 @(cnv_cpm_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
473 | #HT2 #V1 #T1 #HV1 #HT1 #H11 destruct -IH2
474 @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
475 | #m2 #HV2 #H21 #V1 #T1 #HV1 #HT1 #H11 destruct
476 @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
477 | #V2 #T2 #HV2 #HT2 #H21 #HT1 destruct -IH2
478 @ex2_commute @(cnv_cpm_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/
480 @(cnv_cpm_conf_lpr_epsilon_epsilon_aux … IH1) -IH1 /1 width=1 by/
481 | #m2 #HV2 #H21 #HT1 destruct
482 @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
483 | #V2 #T2 #HV2 #HT2 #H21 #m1 #HV1 #H11 destruct
484 @ex2_commute @(cnv_cpm_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
485 | #HT2 #m1 #HV1 #H11 destruct
486 @ex2_commute @(cnv_cpm_conf_lpr_epsilon_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
487 | #m2 #HV2 #H21 #m1 #HV1 #H11 destruct -IH2
488 >minus_S_S >minus_S_S
489 @(cnv_cpm_conf_lpr_ee_ee_aux … IH1) -IH1 /1 width=1 by/