notational change of lift, drop, and gget

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / lpr_lpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 723ed5c5944fa38ea158f0c2980c4f3a32f183e5..284fafe2035b697917901c6a2e24cf80c77aed09 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -31,8 +31,8 @@ fact cpr_conf_lpr_atom_delta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   â\88\80K0,V0. â\87©[i] L0 ≡ K0.ⓓV0 →
-   â\88\80V2. â¦\83G, K0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80T2. â\87§[O, i + 1] V2 ≡ T2 →
+   â\88\80K0,V0. â¬\87[i] L0 ≡ K0.ⓓV0 →
+   â\88\80V2. â¦\83G, K0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80T2. â¬\86[O, i + 1] V2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ #i ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
 #G #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02
@@ -55,10 +55,10 @@ fact cpr_conf_lpr_delta_delta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   â\88\80K0,V0. â\87©[i] L0 ≡ K0.ⓓV0 →
-   â\88\80V1. â¦\83G, K0â¦\84 â\8a¢ V0 â\9e¡ V1 â\86\92 â\88\80T1. â\87§[O, i + 1] V1 ≡ T1 →
-   â\88\80KX,VX. â\87©[i] L0 ≡ KX.ⓓVX →
-   â\88\80V2. â¦\83G, KXâ¦\84 â\8a¢ VX â\9e¡ V2 â\86\92 â\88\80T2. â\87§[O, i + 1] V2 ≡ T2 →
+   â\88\80K0,V0. â¬\87[i] L0 ≡ K0.ⓓV0 →
+   â\88\80V1. â¦\83G, K0â¦\84 â\8a¢ V0 â\9e¡ V1 â\86\92 â\88\80T1. â¬\86[O, i + 1] V1 ≡ T1 →
+   â\88\80KX,VX. â¬\87[i] L0 ≡ KX.ⓓVX →
+   â\88\80V2. â¦\83G, KXâ¦\84 â\8a¢ VX â\9e¡ V2 â\86\92 â\88\80T2. â¬\86[O, i + 1] V2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡ T & ⦃G, L2⦄ ⊢ T2 ➡ T.
 #G #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1
@@ -101,7 +101,7 @@ fact cpr_conf_lpr_bind_zeta:
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
    ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0.ⓓV0⦄ ⊢ T0 ➡ T1 →
-   â\88\80T2. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T2 â\86\92 â\88\80X2. â\87§[O, 1] X2 ≡ T2 →
+   â\88\80T2. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T2 â\86\92 â\88\80X2. â¬\86[O, 1] X2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ +ⓓV1.T1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T.
 #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
@@ -117,8 +117,8 @@ fact cpr_conf_lpr_zeta_zeta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   â\88\80T1. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T1 â\86\92 â\88\80X1. â\87§[O, 1] X1 ≡ T1 →
-   â\88\80T2. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T2 â\86\92 â\88\80X2. â\87§[O, 1] X2 ≡ T2 →
+   â\88\80T1. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T1 â\86\92 â\88\80X1. â¬\86[O, 1] X1 ≡ T1 →
+   â\88\80T2. â¦\83G, L0.â\93\93V0â¦\84 â\8a¢ T0 â\9e¡ T2 â\86\92 â\88\80X2. â¬\86[O, 1] X2 ≡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ X1 ➡ T & ⦃G, L2⦄ ⊢ X2 ➡ T.
 #G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
@@ -193,7 +193,7 @@ elim (cpr_inv_abst1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/ #W #HW1 #HW2
 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/ (**) (* full auto not tried *)
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ (**) (* full auto not tried *)
 /4 width=5 by cpr_bind, cpr_flat, cpr_beta, ex2_intro/
 qed-.
 
@@ -209,7 +209,7 @@ fact cpr_conf_lpr_flat_theta:
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
    ∀V1. ⦃G, L0⦄ ⊢ V0 ➡ V1 → ∀T1. ⦃G, L0⦄ ⊢ ⓓ{a}W0.T0 ➡ T1 →
-   â\88\80V2. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80U2. â\87§[O, 1] V2 ≡ U2 →
+   â\88\80V2. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80U2. â¬\86[O, 1] V2 ≡ U2 →
    ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ ⓐV1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T.
@@ -246,8 +246,8 @@ fact cpr_conf_lpr_beta_beta:
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1/ #W #HW1 #HW2
 elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
-lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_abst/
-lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_abst/
+lapply (lsubr_cpr_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/
+lapply (lsubr_cpr_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/
 /4 width=5 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
@@ -259,9 +259,9 @@ fact cpr_conf_lpr_theta_theta:
       ∀L1. ⦃G, L⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L⦄ ⊢ ➡ L2 →
       ∃∃T0. ⦃G, L1⦄ ⊢ T1 ➡ T0 & ⦃G, L2⦄ ⊢ T2 ➡ T0
    ) →
-   â\88\80V1. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V1 â\86\92 â\88\80U1. â\87§[O, 1] V1 ≡ U1 →
+   â\88\80V1. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V1 â\86\92 â\88\80U1. â¬\86[O, 1] V1 ≡ U1 →
    ∀W1. ⦃G, L0⦄ ⊢ W0 ➡ W1 → ∀T1. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T1 →
-   â\88\80V2. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80U2. â\87§[O, 1] V2 ≡ U2 →
+   â\88\80V2. â¦\83G, L0â¦\84 â\8a¢ V0 â\9e¡ V2 â\86\92 â\88\80U2. â¬\86[O, 1] V2 ≡ U2 →
    ∀W2. ⦃G, L0⦄ ⊢ W0 ➡ W2 → ∀T2. ⦃G, L0.ⓓW0⦄ ⊢ T0 ➡ T2 →
    ∀L1. ⦃G, L0⦄ ⊢ ➡ L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡ L2 →
    ∃∃T. ⦃G, L1⦄ ⊢ ⓓ{a}W1.ⓐU1.T1 ➡ T & ⦃G, L2⦄ ⊢ ⓓ{a}W2.ⓐU2.T2 ➡ T.