- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / lfpr_lfpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
index d05584ebf795bae07dd1c19000b10b2c894f31ce..7c6c22237058b6f64d9af569300d6e044f9fb72f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
@@ -45,10 +45,11 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_
 lapply (drops_isuni_fwd_drop2 … HLK2) // -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2
 /3 width=6 by cpm_delta_drops, ex2_intro/
 qed-.
 
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_delta_delta:
    ∀h,G,L0,i. (
       ∀L,T. ⦃G, L0, #i⦄ ⊐+ ⦃G, L, T⦄ →
@@ -71,8 +72,8 @@ elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_
 lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
-elim (cpm_lifts … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
-elim (cpm_lifts … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
+elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1
+elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2
 lapply (lifts_mono … HX … HVT) #H destruct
 /2 width=3 by ex2_intro/
 qed-.
@@ -113,9 +114,10 @@ fact cpr_conf_lfpr_bind_zeta:
 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/
 qed-.
 
+(* Note: we don't use cpm_inv_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_zeta_zeta:
    ∀h,G,L0,V0,T0. (
       ∀L,T. ⦃G, L0, +ⓓV0.T0⦄ ⊐+ ⦃G, L, T⦄ →
@@ -132,8 +134,8 @@ fact cpr_conf_lfpr_zeta_zeta:
 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0
 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0
 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -T0 #T #HT1 #HT2
-elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
-elim (cpm_inv_lifts1 … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
+elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1
+elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2
 lapply (lifts_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
 qed-.
 
@@ -234,7 +236,7 @@ elim (lfpr_inv_bind … HL01) -HL01 #H1W0 #H1T0
 elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02
 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0
 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #U #HVU #HU2
 elim (cpm_inv_abbr1 … H) -H *
 [ #W1 #T1 #HW01 #HT01 #H destruct
   elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
@@ -242,7 +244,7 @@ elim (cpm_inv_abbr1 … H) -H *
   /4 width=7 by cpm_bind, cpr_flat, cpm_theta, ex2_intro/
 | #T1 #HT01 #HXT1 #H destruct
   elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-  elim (cpm_inv_lifts1 … HT1 … L1 … HXT1) -HXT1
+  elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -HXT1
   /4 width=9 by cpr_flat, cpm_zeta, drops_refl, drops_drop, lifts_flat, ex2_intro/
 ]
 qed-.
@@ -272,6 +274,7 @@ lapply (lsubr_cpm_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_bet
 /4 width=5 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
+(* Note: we don't use cpm_lifts_bi to preserve visual symmetry *)
 fact cpr_conf_lfpr_theta_theta:
    ∀h,p,G,L0,V0,W0,T0. (
       ∀L,T. ⦃G, L0, ⓐV0.ⓓ{p}W0.T0⦄ ⊐+ ⦃G, L, T⦄ →
@@ -294,8 +297,8 @@ elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0
 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/
 elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0
-elim (cpm_lifts … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
-elim (cpm_lifts … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
+elim (cpm_lifts_sn … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU
+elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX
 lapply (lifts_mono … HX … HVU) -HX #H destruct
 /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.