matita/matita/contribs/lambdadelta/basic_2/etc/cnv/cnv_cpm_tdeq1_conf.etc

   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 "basic_2/rt_transition/cpm_lsubr.ma".
  16 include "basic_2/rt_transition/lpr_drops.ma".
  17 include "basic_2/dynamic/cnv_drops.ma".
  18 include "basic_2/dynamic/cnv_cpm_tdeq.ma".
  19 include "basic_2/dynamic/cnv_preserve_sub.ma".
  20
  21 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
  22
  23 definition IH_cnv_cpm_tdeq1_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
  24                                      λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
  25                                      ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
  26                                      ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
  27                                      ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
  28                                      ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
  29
  30 definition IH_cnv_cpms_tdeq1_strip_lpr (a) (h) (o): relation3 genv lenv term ≝
  31                                        λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
  32                                        ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
  33                                        ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
  34                                        ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → L0 ≛[h, o, T0] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
  35                                        ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
  36
  37 definition IH_cnv_cpm_tdeq2_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
  38                                      λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
  39                                      ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
  40                                      ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 → T0 ≛[h,o] T2 →
  41                                      ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
  42                                      ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
  43
  44 definition IH_cnv_cpm_tdeq2_strip_lpr (a) (h) (o): relation3 genv lenv term ≝
  45                                       λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
  46                                       ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → T0 ≛[h,o] T1 →
  47                                       ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 → T0 ≛[h,o] T2 →
  48                                       ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
  49                                       ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & T1 ≛[h,o] T & ⦃G, L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
  50
  51 include "ground_2/lib/arith_2b.ma".
  52 include "basic_2/rt_computation/cpms_rdeq.ma".
  53 include "basic_2/rt_computation/cpms_fpbg.ma".
  54
  55 fact cnv_cpms_tdeq1_strip_lpr_sub (a) (h) (o):
  56                                   ∀G0,L0,T0.
  57                                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
  58                                   (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) →
  59                                   ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_tdeq1_strip_lpr a h o G1 L1 T1.
  60 #a #h #o #G #L #T #IH2 #IH1 #G0 #L0 #T0 #H0 #HT0 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H @(cpms_ind_dx … H) -n2 -T2
  61 [ #L1 #H1L01 #H2L01 #L2 #HL02 -IH2
  62   elim (IH1 … H1T01 H2T01 0 T0 … L1 … L2) // -L0 -IH1 -H2T01 #T3 #HT13 #H1T03 #H2T03
  63   /3 width=4 by cpm_cpms, ex3_intro/
  64 | #n #n2 #X2 #T2 #HX2 #IHX2 #HXT2 #L1 #H1L01 #H2L01 #L2 #HL02 -H1T01 -H2T01
  65   elim (IHX2 L1 … L0) -IHX2 // #X1 #HTX1 #H1X21 #H2X21
  66   elim (IH1 … H1X21 H2X21 … HXT2 L1 … L2)
  67   [|*: /3 width=12 by cnv_cpms_trans_lpr_sub, fpbg_cpms_trans, cpms_rdeq_conf_sn/ ] -X2 -IH1 -IH2 #X2 #HX12 #H1TX2 #H2TX2
  68   >arith_l3 @(ex3_intro … H2TX2) /2 width=3 by cpms_step_dx/ (**) (* explict constructor *)
  69 ]
  70 qed-.
  71
  72 (* Sub diamond propery with restricted rt-transition for terms **************)
  73
  74 fact cnv_cpm_tdeq1_conf_lpr_atom_atom_aux (h) (o) (G) (L1) (L2) (I):
  75      ∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡[O,h] T & ⓪{I} ≛[h,o] T.
  76 /2 width=4 by ex3_intro/ qed-.
  77
  78 fact cnv_cpm_tdeq1_conf_lpr_atom_ess_aux (h) (o) (G) (L1) (L2) (s):
  79      ∃∃T. ⦃G,L1⦄ ⊢ ⋆s ➡[1,h] T & ⦃G,L2⦄ ⊢ ⋆(next h s) ➡[h] T & ⋆(next h s) ≛[h,o] T.
  80 /2 width=4 by ex3_intro/ qed-.
  81
  82 fact cnv_cpm_tdeq1_conf_lpr_ess_atom_aux (h) (o) (G) (L1) (L2) (s):
  83      deg h o s 0 →
  84      ∃∃T. ⦃G,L1⦄ ⊢ ⋆(next h s) ➡[h] T & ⦃G,L2⦄ ⊢⋆s ➡[1,h] T & ⋆s ≛[h,o] T.
  85 /4 width=6 by tdeq_sort, deg_next, ex3_intro/ qed-.
  86
  87 fact cnv_cpm_tdeq1_conf_lpr_atom_delta_aux (a) (h) (o) (G) (L) (i):
  88      (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
  89      ⦃G,L⦄ ⊢ #i ![a,h] →
  90      ∀K,V. ⬇*[i]L ≘ K.ⓓV →
  91      ∀n,XV. ⦃G,K⦄ ⊢ V ➡[n,h] XV →
  92      ∀X. ⬆*[↑i]XV ≘ X →
  93      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
  94      ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T.
  95 #a #h #o #G #L #i #IH #HT #K #V #HLK #n #XV #HVX #X #HXV #L1 #H1L1 #H2L1 #L2 #HL2
  96 lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HV
  97 elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1
  98 elim (lpr_inv_pair_sn … H1) -H1 #K1 #V1 #H1K1 #H1V1 #H destruct
  99 elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2V1 #_
 100 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
 101 elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
 102 lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
 103 lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
 104 elim (IH … H1V1 H2V1 … HVX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
 105 <minus_O_n <minus_n_O #V #HV1 #H1VX #H2VX
 106 elim (cpm_lifts_sn … H1VX … HLK2 … HXV) -H1VX -HLK2 #VX #HVX #HXVX
 107 lapply (tdeq_lifts_bi … H2VX … HXV … HVX) -H2VX -HXV #H2VX
 108 /3 width=6 by cpm_delta_drops, ex3_intro/
 109 qed-.
 110
 111 fact cnv_cpm_tdeq1_conf_lpr_atom_ell_aux (a) (h) (o) (G) (L) (i):
 112      (∀G0,L0,T0. ⦃G,L,#i⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 113      ⦃G,L⦄⊢#i![a,h] →
 114      ∀K,W. ⬇*[i]L ≘ K.ⓛW →
 115      ∀n,XW. ⦃G,K⦄ ⊢ W ➡[n,h] XW →
 116      ∀X. ⬆*[↑i]XW ≘ X →
 117      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,#i] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 118      ∃∃T. ⦃G,L1⦄ ⊢ #i ➡[↑n,h] T & ⦃G,L2⦄ ⊢ X ➡[h] T & X ≛[h,o] T.
 119 #a #h #o #G #L #i #IH #HT #K #W #HLK #n #XW #HWX #X #HXW #L1 #H1L1 #H2L1 #L2 #HL2
 120 lapply (cnv_lref_fwd_drops … HT … HLK) -HT #HW
 121 elim (lpr_drops_conf … HLK … H1L1) -H1L1 // #Y1 #H1 #HLK1
 122 elim (lpr_inv_pair_sn … H1) -H1 #K1 #W1 #H1K1 #H1W1 #H destruct
 123 elim (rdeq_inv_lref_pair_bi … H2L1 … HLK … HLK1) -H2L1 #H2K1 #H2W1 #_
 124 elim (lpr_drops_conf … HLK … HL2) -HL2 // #Y2 #H2 #HLK2
 125 elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct
 126 lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
 127 lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
 128 elim (IH … H1W1 H2W1 … HWX … H1K1 H2K1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
 129 <minus_O_n <minus_n_O #W #HW1 #H1WX #H2WX
 130 elim (cpm_lifts_sn … H1WX … HLK2 … HXW) -H1WX -HLK2 #WX #HWX #HXWX
 131 lapply (tdeq_lifts_bi … H2WX … HXW … HWX) -H2WX -HXW #H2WX
 132 /3 width=6 by cpm_ell_drops, ex3_intro/
 133 qed-.
 134
 135 fact cnv_cpm_tdeq1_conf_lpr_bind_bind_aux (a) (h) (o) (p) (I) (G) (L) (V) (T):
 136      (∀G0,L0,T0. ⦃G,L,ⓑ{p,I}V.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 137      ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![a,h] →
 138      ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
 139      ∀n1,T1. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
 140      ∀n2,T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T ➡[n2,h] T2 →
 141      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓑ{p,I}V.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 142      ∃∃T. ⦃G,L1⦄ ⊢ ⓑ{p,I}V.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓑ{p,I}V2.T2 ➡[n1-n2,h] T & ⓑ{p,I}V2.T2 ≛[h,o] T.
 143 #a #h #o #p #I #G0 #L0 #V0 #T0 #IH #H0
 144 #V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02
 145 #L1 #H1L01 #H2L01 #L2 #HL02
 146 elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
 147 elim (rdeq_inv_bind … H2L01) -H2L01 #H0L01 #H2L01
 148 elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 149 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
 150 elim (IH … H1T01 H2T01 … HT02 (L1.ⓑ{I}V0) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
 151 #T #HT1 #H1T2 #H2T2 -L0 -T0
 152 /3 width=6 by cpm_bind, tdeq_pair, ex3_intro/
 153 qed-.
 154
 155 fact cnv_cpm_tdeq1_conf_lpr_bind_zeta_aux (a) (h) (o) (G) (L) (V) (T):
 156      (∀G0,L0,T0. ⦃G,L,+ⓓV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 157      ⦃G,L⦄ ⊢ +ⓓV.T ![a,h] →
 158      ∀n1,T1. ⦃G,L.ⓓV⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
 159      ∀T2. ⬆*[1]T2 ≘ T → ∀n2,XT2. ⦃G,L⦄ ⊢ T2 ➡[n2,h] XT2 →
 160      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,+ⓓV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 161      ∃∃T. ⦃G,L1⦄ ⊢ +ⓓV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ XT2 ➡[n1-n2,h] T & XT2 ≛[h,o] T.
 162 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
 163 #n1 #T1 #H1T01 #H2T01 #T2 #HT20 #n2 #XT2 #HXT2
 164 #L1 #H1L01 #H2L01 #L2 #HL02
 165 elim (cnv_inv_bind … H0) -H0 #_ #HT0
 166 elim (rdeq_inv_bind … H2L01) -H2L01 #_ #H2L01
 167 lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
 168 [ /3 width=3 by drops_refl, drops_drop/ ] #HT2
 169 elim (cpm_inv_lifts_sn … H1T01 (Ⓣ) … L0 … HT20) -H1T01
 170 [| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #H1XT12
 171 lapply (tdeq_inv_lifts_bi … H2T01 … HT20 … HXT1) -H2T01 #H2XT12
 172 lapply (rdeq_inv_lifts_bi … H2L01 (Ⓣ) … L0 L1 … HT20) -H2L01
 173 [4:|*: /3 width=1 by drops_refl, drops_drop/ ] #H2L01
 174 elim (IH … H1XT12 H2XT12 … HXT2 … H1L01 … HL02)
 175 [|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #H1T2 #H2T2
 176 /3 width=4 by cpm_zeta, ex3_intro/
 177 qed-.
 178
 179 fact cnv_cpm_tdeq1_conf_lpr_appl_appl_aux (a) (h) (o) (G) (L) (V) (T):
 180      (∀G0,L0,T0. ⦃G,L,ⓐV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 181      ⦃G,L⦄ ⊢ ⓐV.T ![a,h] →
 182      ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 →
 183      ∀n1,T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
 184      ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
 185      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 186      ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓐV2.T2 ➡[n1-n2,h] T & ⓐV2.T2 ≛[h,o] T.
 187 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
 188 #V2 #HV02 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #HT02
 189 #L1 #H1L01 #H2L01 #L2 #HL02
 190 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
 191 elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
 192 elim (IH … V0 … 0 V0 … HV02 … H1L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 193 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
 194 elim (IH … H1T01 H2T01 … HT02 … H1L01 H2L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 195 #T #HT1 #H1T2 #H2T2 -L0 -T0
 196 /3 width=6 by cpm_appl, tdeq_pair, ex3_intro/
 197 qed-.
 198
 199 fact cnv_cpm_tdeq1_conf_lpr_appl_beta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
 200      (∀G0,L0,T0. ⦃G,L,ⓐV.ⓛ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 201      ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.T ![a,h] →
 202      ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
 203      ∀n1,T1. ⦃G,L⦄ ⊢ ⓛ{p}W.T ➡[n1,h] T1 → ⓛ{p}W.T ≛[h,o] T1 →
 204      ∀n2,T2. ⦃G,L.ⓛW⦄ ⊢ T ➡[n2,h] T2 →
 205      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓛ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 206      ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}ⓝW2.V2.T2 ➡[n1-n2,h] T & ⓓ{p}ⓝW2.V2.T2 ≛[h,o] T.
 207 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 208 #V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02
 209 #L1 #H1L01 #H2L01 #L2 #HL02
 210 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
 211 elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
 212 elim (cpm_inv_abst1 … H1X) -H1X #W1 #T1 #H1W01 #H1T01 #H destruct
 213 elim (tdeq_inv_pair … H2X) -H2X #_ #H2W01 #H2T01
 214 elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
 215 elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01
 216 elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 217 -HV0 -HV02 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
 218 elim (IH … H1W01 H2W01 … HW02 … H1L01 H3L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 219 -HW0 <minus_n_O #W #HW1 #H1W2 #H2W2
 220 elim (IH … H1T01 H2T01 … HT02 (L1.ⓛW1) … (L2.ⓛW2))
 221 [|*: /3 width=2 by fqup_fpbg, lpr_pair, rdeq_bind_repl_dx, ext2_pair/ ]
 222 #T #HT1 #H1T2 #H2T02 -L0 -W0 -T0
 223 lapply (lsubr_cpm_trans … H1T2 (L2.ⓓⓝW2.V2) ?) -H1T2 [ /2 width=1 by lsubr_beta/ ] #H1T2
 224 /4 width=6 by cpm_beta, cpm_cast, cpm_bind, tdeq_pair, ex3_intro/
 225 qed-.
 226
 227 fact cnv_cpm_tdeq1_conf_lpr_appl_theta_aux (a) (h) (o) (p) (G) (L) (V) (W) (T):
 228      (∀G0,L0,T0. ⦃G,L,ⓐV.ⓓ{p}W.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 229      ⦃G,L⦄ ⊢ ⓐV.ⓓ{p}W.T ![a,h] →
 230      ∀V2. ⦃G,L⦄ ⊢ V ➡[h] V2 → ∀W2. ⦃G,L⦄ ⊢ W ➡[h] W2 →
 231      ∀n1,T1. ⦃G,L⦄ ⊢ ⓓ{p}W.T ➡[n1,h] T1 → ⓓ{p}W.T ≛[h,o] T1 →
 232      ∀n2,T2. ⦃G,L.ⓓW⦄ ⊢ T ➡[n2,h] T2 → ∀U2. ⬆*[1]V2 ≘ U2 →
 233      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓐV.ⓓ{p}W.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 234      ∃∃T. ⦃G,L1⦄ ⊢ ⓐV.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓓ{p}W2.ⓐU2.T2 ➡[n1-n2,h] T & ⓓ{p}W2.ⓐU2.T2 ≛[h,o] T.
 235 #a #h #o #p #G0 #L0 #V0 #W0 #T0 #IH #H0
 236 #V2 #HV02 #W2 #HW02 #n1 #X #H1X #H2X #n2 #T2 #HT02 #U2 #HVU2
 237 #L1 #H1L01 #H2L01 #L2 #HL02
 238 elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #H0 #_ #_ -n0 -p0 -X01 -X02
 239 elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T1 #HW0 #HT0 #H1T01 #H2T01 #H destruct
 240 elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
 241 elim (rdeq_inv_bind … H2L01) -H2L01 #H3L01 #H2L01
 242 elim (IH … V0 … 0 V0 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 243 -HV0 -HV02 -H0L01 <minus_n_O #V #HV1 #H1V2 #H2V2
 244 elim (IH … W0 … 0 W0 … HW02 … H1L01 H3L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 245 -HW0 <minus_n_O #W #HW1 #H1W2 #H2W2
 246 elim (IH … H1T01 H2T01 … HT02 (L1.ⓓW0) … (L2.ⓓW2))
 247 [|*: /3 width=2 by fqup_fpbg, lpr_bind_refl_dx, lpr_bind, ext2_pair/ ]
 248 #T #HT1 #H1T2 #H2T02 -L0 -T0
 249 elim (cpm_lifts_sn … H1V2 (Ⓣ) … (L2.ⓓW2) … HVU2) -H1V2
 250 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #H1U2
 251 lapply (tdeq_lifts_bi … H2V2 … HVU2 … HVU) -H2V2 #H2U2
 252 /4 width=8 by cpm_theta, cpm_appl, cpm_bind, tdeq_pair, ex3_intro/
 253 qed-.
 254
 255 fact cnv_cpm_tdeq1_conf_lpr_cast_cast_aux (a) (h) (o) (G) (L) (V) (T):
 256      (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 257      ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
 258      ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
 259      ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
 260      ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
 261      ∀T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
 262      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 263      ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ ⓝV2.T2 ➡[n1-n2,h] T & ⓝV2.T2≛[h,o]T.
 264 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
 265 #n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01 #T2 #HT02
 266 #L1 #H1L01 #H2L01 #L2 #HL02
 267 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
 268 elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
 269 elim (IH … H1V01 H2V01 … HV02 … H1L01 H0L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 270 elim (IH … H1T01 H2T01 … HT02 … H1L01 H2L01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 271 #T #HT1 #H1T2 #H2T2 #V #HV1 #H1V2 #H2V2 -L0 -V0 -T0
 272 /3 width=6 by cpm_cast, tdeq_pair, ex3_intro/
 273 qed-.
 274 (*
 275 fact cnv_cpm_tdeq1_conf_lpr_cast_epsilon_aux (a) (h) (o) (G) (L) (V) (T):
 276      (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 277      ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
 278      ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
 279      ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o] T1 →
 280      ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
 281      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T] L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 282      ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[n2-n1,h] T & ⦃G,L2⦄ ⊢ T2 ➡[n1-n2,h] T & T2 ≛[h,o] T.
 283 #a #h #o #G0 #L0 #V0 #T0 #IH #H0
 284 #n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
 285 #L1 #HL01 #L2 #HL02
 286 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
 287 elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 288 #T #HT1 #HT2 -L0 -V0 -T0
 289 /3 width=3 by cpms_eps, ex2_intro/
 290 qed-.
 291 *)
 292 fact cnv_cpm_tdeq1_conf_lpr_cast_ee_aux (a) (h) (o) (G) (L) (V) (T):
 293      (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_trans_lpr a h G0 L0 T0) →
 294      (∀G0,L0,T0. ⦃G,L,ⓝV.T⦄ >[h,o] ⦃G0,L0,T0⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G0 L0 T0) →
 295      ⦃G,L⦄ ⊢ ⓝV.T ![a,h] →
 296      ∀n1,V1. ⦃G,L⦄ ⊢ V ➡[n1,h] V1 → V ≛[h,o] V1 →
 297      ∀n2,V2. ⦃G,L⦄ ⊢ V ➡[n2,h] V2 →
 298      ∀T1. ⦃G,L⦄ ⊢ T ➡[n1,h] T1 → T ≛[h,o]T1 →
 299      ∀L1. ⦃G,L⦄ ⊢ ➡[h] L1 → L ≛[h,o,ⓝV.T]L1 → ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 →
 300      ∃∃T. ⦃G,L1⦄ ⊢ ⓝV1.T1 ➡[↑n2-n1,h] T & ⦃G,L2⦄ ⊢ V2 ➡[n1-↑n2,h] T & V2 ≛[h,o] T.
 301 #a #h #o #G0 #L0 #V0 #T0 #IH2 #IH1 #H0
 302 #n1 #V1 #H1V01 #H2V01 #n2 #V2 #HV02 #T1 #H1T01 #H2T01
 303 #L1 #H1L01 #H2L01 #L2 #HL02
 304 (* n2=0 n1=1 *)
 305  -H1V01 -H2V01
 306 elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
 307 elim (rdeq_inv_flat … H2L01) -H2L01 #H0L01 #H2L01
 308 lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
 309 elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
 310 elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
 311 -HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
 312 elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
 313 -L0 -V0 -T0 -X0 #U #HVU #HTU
 314 lapply (cpms_trans … HV2 … HVU) -V <plus_O_n >minus_plus #H2
 315 lapply (cpms_trans … HT1 … HTU) -T <arith_l2 #H1
 316 /3 width=3 by cpms_eps, ex2_intro/
 317 qed-.
 318
 319 fact cnv_cpm_tdeq1_conf_lpr_aux (a) (h) (o):
 320                                 ∀G0,L0,T0.
 321                                 (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
 322                                 (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1) →
 323                                 ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_tdeq1_conf_lpr a h o G1 L1 T1.
 324 #a #h #o #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
 325 [ #I #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
 326   elim (cpm_tdeq_inv_atom_sn … H1X1 H2X1) -H1X1 -H2X1 *
 327   elim (cpm_inv_atom1_drops … HX2) -HX2 *
 328   [ #H21 #H22 #H11 #H12 destruct -a -L
 329     <minus_O_n
 330     /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_atom_aux/
 331   | #s2 #H21 #H22 #H23 #H11 #H12 destruct -a -L
 332     <minus_O_n <minus_n_O
 333     /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_ess_aux/
 334   | #K2 #V2 #XV2 #i #HLK2 #HVX2 #HXV2 #H21 #H11 #H12 destruct -IH2
 335     <minus_O_n <minus_n_O
 336     @(cnv_cpm_tdeq1_conf_lpr_atom_delta_aux … IH1) -IH1 /1 width=6 by/
 337   | #m2 #K2 #W2 #XW2 #i #HLK2 #HWX2 #HXW2 #H21 #H22 #H11 #H12 destruct -IH2
 338     <minus_O_n <minus_n_O
 339     @(cnv_cpm_tdeq1_conf_lpr_atom_ell_aux … IH1) -IH1 /1 width=6 by/
 340   | #H21 #H22 #s1 #H11 #H12 #H13 #H14 destruct -a -L
 341     <minus_O_n <minus_n_O
 342     /2 width=1 by cnv_cpm_tdeq1_conf_lpr_ess_atom_aux/
 343   | #s2 #H21 #H22 #H23 #s1 #H11 #H12 #H13 #_ destruct -a -L
 344     <minus_n_n
 345     /2 width=1 by cnv_cpm_tdeq1_conf_lpr_atom_atom_aux/
 346   | #K2 #V2 #XV2 #i2 #_ #_ #_ #H21 #s1 #H11 #H12 #H13 #_ destruct
 347   | #m2 #K2 #W2 #XW2 #i2 #_ #_ #_ #H21 #H22 #s1 #H11 #H12 #H13 #_ destruct
 348   ]
 349 | #p #I #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
 350   elim (cpm_tdeq_inv_bind_sn … HT … H1X1 H2X1) -H1X1 -H2X1
 351   elim (cpm_inv_bind1 … HX2) -HX2 *
 352   [ #V2 #T2 #HV2 #HT2 #H21 #T1 #_ #_ #H1T1 #H2T1 #H11 destruct -IH2
 353     @(cnv_cpm_tdeq1_conf_lpr_bind_bind_aux … IH1) -IH1 /1 width=1 by/
 354   | #T2 #HT2 #HTX2 #H21 #H22 #T1 #_ #_ #H1T1 #H2T1 #H11 destruct -IH2
 355     @(cnv_cpm_tdeq1_conf_lpr_bind_zeta_aux … IH1) -IH1 /1 width=3 by/
 356   ]
 357 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
 358   elim (cpm_tdeq_inv_appl_sn … HT … H1X1 H2X1) -H1X1 -H2X1
 359   elim (cpm_inv_appl1 … HX2) -HX2 *
 360   [ #V2 #T2 #HV2 #HT2 #H21 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
 361     @(cnv_cpm_tdeq1_conf_lpr_appl_appl_aux … IH1) -IH1 /1 width=1 by/
 362   | #p2 #V2 #XW2 #W2 #XT2 #T2 #HV2 #HW2 #HT2 #H21 #H22 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
 363     @(cnv_cpm_tdeq1_conf_lpr_appl_beta_aux … IH1) -IH1 /1 width=1 by/
 364   | #p2 #V2 #XV2 #XW2 #W2 #XT2 #T2 #HV2 #HXV2 #HW2 #HT2 #H21 #H22 #m #q #W1 #U1 #T1 #_ #_ #_ #_ #_ #H1T1 #H2T1 #H11 destruct -IH2 -m -q -W1 -U1
 365     @(cnv_cpm_tdeq1_conf_lpr_appl_theta_aux … IH1) -IH1 /1 width=3 by/
 366   ]
 367 | #V #T #HG0 #HL0 #HT0 #HT #n1 #X1 #H1X1 #H2X1 #n2 #X2 #HX2 #L1 #H1L1 #H2L1 #L2 #HL2 destruct
 368   elim (cpm_tdeq_inv_cast_sn … HT … H1X1 H2X1) -H1X1 -H2X1
 369   elim (cpm_inv_cast1 … HX2) -HX2 [ * || * ]
 370   [ #V2 #T2 #HV2 #HT2 #H21 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -IH2 -U1
 371     @(cnv_cpm_tdeq1_conf_lpr_cast_cast_aux … IH1) -IH1 /1 width=1 by/
 372   | #HT2 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -IH2 -U1
 373 (*    @(cnv_cpm_tdeq1_conf_lpr_cast_epsilon_aux … IH1) -IH1 /1 width=1 by/ *)
 374   | #m2 #HV2 #H21 #U1 #V1 #T1 #_ #_ #_ #H1V1 #H2V1 #_ #H1T1 #H2T1 #H11 destruct -U1
 375     @(cnv_cpm_tdeq1_conf_lpr_cast_ee_aux … IH2 IH1) -IH2 -IH1 /1 width=1 by/
 376   ]
 377 ]