matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc

   1 include "basic_2/rt_transition/lpr.ma".
   2 include "basic_2/rt_conversion/lpce.ma".
   3 include "basic_2/dynamic/cnv_preserve.ma".
   4
   5 lemma cpce_cpm_conf_lpce_lpr (a) (h) (n) (G):
   6       ∀L1,T1. ⦃G,L1⦄ ⊢ T1 ![a,h] →
   7       ∀U1. ⦃G,L1⦄ ⊢ T1 ⬌η[h] U1 → ∀K1. ⦃G,L1⦄ ⊢ ⬌η[h] K1 →
   8       ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 →
   9       ∃∃K2,U2.  ⦃G,K1⦄ ⊢ ➡[h] K2 & ⦃G,L2⦄ ⊢ ⬌η[h] K2 & ⦃G,K2⦄ ⊢ U1 ➡[n,h] U2 & ⦃G,L2⦄ ⊢ T2 ⬌η[h] U2.
  10 #a #h #n #G #L1 #T1 #HT1
  11 letin o ≝ (sd_O h)
  12 lapply (cnv_fwd_fsb … o … HT1) -HT1 #H
  13 @(fsb_ind_fpbg … H) -G -L1 -T1 #G #L1 #T1 #_ #IH
  14 #U1
  15
  16 #H elim H -G -L1 -T1 -U1
  17 [ #G #L1 elim L1 -L1 [| #L1 #I1 #IH ] #s #K1 #HLK1 #X2 #HX2 #Y2 #HY2
  18   elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn destruct
  19   [ lapply (lpr_inv_atom_sn … HY2) -HY2 #H destruct
  20     lapply (lpce_inv_atom_sn … HLK1) -HLK1 #H destruct
  21     /3 width=6 by cpce_sort, cpm_sort, ex4_2_intro/
  22   | elim (lpr_inv_bind_sn … HY2) -HY2 #I2 #L2 #HL12 #HI12 #H destruct
  23     elim (lpce_inv_bind_sn … HLK1) -HLK1 #J1 #K0 #HLK1 #HIJ1 #H destruct
  24     elim (IH s ? HLK1 (⋆((next h)^n s)) … HL12) -IH -HLK1 -HL12
  25     [| /2 width=1 by cpm_sort/ ] #K2 #U2 #HK12 #HLK2 #H1s #H2s
  26
  27 | #G #L1 #s elim L1 -L1
  28   [ #Y2 #HY2 #X2 #HX2 #K1 #HLK1
  29     lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
  30     /3 width=6 by cpce_sort, ex4_2_intro/
  31   | #L1 #I1 #IH #Y2 #HY2 #X2 #HX2 #K1 #HLK1
  32     lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
  33
  34
  35 | #n #G #K1 #V1 #V2 #X1 #HV12 #_ #HX1 #X2 #HX2 #Y2 #HY2
  36   elim (lpr_inv_pair_sn … HY2) -HY2 #K2 #W1 #HK12 #HVW1 #H destruct
  37   lapply (cpce_inv_ldef_sn … HX2) -HX2 #H destruct
  38   elim (lifts_total W1 (𝐔❴1❵)) #X2 #HX2
  39   @(ex2_intro … X2) [ @(cpm_delta … HX2) /3 width=5 by _/
  40
  41   /3 width=3 by cpce_ldef, ex2_intro/
  42   |