matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_conf.ma

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