include "basic_2/rt_transition/lpr.ma".
include "basic_2/rt_conversion/lpce.ma".
include "basic_2/dynamic/cnv_preserve.ma".

lemma cpce_cpm_conf_lpce_lpr (a) (h) (n) (G):
      ∀L1,T1. ⦃G,L1⦄ ⊢ T1 ![a,h] →
      ∀U1. ⦃G,L1⦄ ⊢ T1 ⬌η[h] U1 → ∀K1. ⦃G,L1⦄ ⊢ ⬌η[h] K1 →
      ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 →
      ∃∃K2,U2.  ⦃G,K1⦄ ⊢ ➡[h] K2 & ⦃G,L2⦄ ⊢ ⬌η[h] K2 & ⦃G,K2⦄ ⊢ U1 ➡[n,h] U2 & ⦃G,L2⦄ ⊢ T2 ⬌η[h] U2.
#a #h #n #G #L1 #T1 #HT1
letin o ≝ (sd_O h)
lapply (cnv_fwd_fsb … o … HT1) -HT1 #H
@(fsb_ind_fpbg … H) -G -L1 -T1 #G #L1 #T1 #_ #IH
#U1 

#H elim H -G -L1 -T1 -U1
[ #G #L1 elim L1 -L1 [| #L1 #I1 #IH ] #s #K1 #HLK1 #X2 #HX2 #Y2 #HY2
  elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn destruct
  [ lapply (lpr_inv_atom_sn … HY2) -HY2 #H destruct
    lapply (lpce_inv_atom_sn … HLK1) -HLK1 #H destruct
    /3 width=6 by cpce_sort, cpm_sort, ex4_2_intro/
  | elim (lpr_inv_bind_sn … HY2) -HY2 #I2 #L2 #HL12 #HI12 #H destruct
    elim (lpce_inv_bind_sn … HLK1) -HLK1 #J1 #K0 #HLK1 #HIJ1 #H destruct
    elim (IH s ? HLK1 (⋆((next h)^n s)) … HL12) -IH -HLK1 -HL12
    [| /2 width=1 by cpm_sort/ ] #K2 #U2 #HK12 #HLK2 #H1s #H2s

| #G #L1 #s elim L1 -L1
  [ #Y2 #HY2 #X2 #HX2 #K1 #HLK1
    lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
    /3 width=6 by cpce_sort, ex4_2_intro/
  | #L1 #I1 #IH #Y2 #HY2 #X2 #HX2 #K1 #HLK1
    lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct

    
| #n #G #K1 #V1 #V2 #X1 #HV12 #_ #HX1 #X2 #HX2 #Y2 #HY2
  elim (lpr_inv_pair_sn … HY2) -HY2 #K2 #W1 #HK12 #HVW1 #H destruct
  lapply (cpce_inv_ldef_sn … HX2) -HX2 #H destruct
  elim (lifts_total W1 (𝐔❴1❵)) #X2 #HX2
  @(ex2_intro … X2) [ @(cpm_delta … HX2) /3 width=5 by _/
  
  /3 width=3 by cpce_ldef, ex2_intro/
  |