update in basic_2

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
index bc6e8a43ab0522bf1ea62fe6e1981a8594997367..6dc8c19467d9c005449c2b6ed5ab295c56366c87 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma
@@ -16,7 +16,7 @@ include "basic_2/static/aaa_drops.ma".
 include "basic_2/static/lsuba_aaa.ma".
 include "basic_2/rt_transition/lfpx_fqup.ma".
 
-(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+(* UNBOUND PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *******)
 
 (* Properties with atomic arity assignment for terms ************************)
 
@@ -34,9 +34,9 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
   [ #H destruct /3 width=1 by aaa_zero/
   | -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
   ]
-| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY
-  elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct
-  elim (cpx_inv_lref1_pair … HX) -HX
+| #I #G #L1 #B #i #_ #IH #X2 #HX #Y #HY
+  elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #L2 #HL12 #H destruct
+  elim (cpx_inv_lref1_bind … HX) -HX
   [ #H destruct /3 width=1 by aaa_lref/
   | * /4 width=7 by aaa_lifts, drops_refl, drops_drop/
   ]
@@ -44,14 +44,14 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
   elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
   elim (cpx_inv_abbr1 … HX) -HX *
   [ #V2 #T2 #HV12 #HT12 #H destruct
-    /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/
+    /5 width=2 by lfpx_bind_repl_dx, aaa_abbr, ext2_pair/
   | #T2 #HT12 #HXT2 #H destruct -IHV
     /4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/
   ]
 | #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
   elim (lfpx_inv_bind … HL12) -HL12 #HV #HT
   elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
-  /4 width=2 by lfpx_pair_repl_dx, aaa_abst/
+  /5 width=2 by lfpx_bind_repl_dx, aaa_abst, ext2_pair/
 | #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12
   elim (lfpx_inv_flat … HL12) -HL12 #HV #HT
   elim (cpx_inv_appl1 … H) -H *
@@ -73,10 +73,9 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
 ]
 qed-.
 
-lemma cpx_aaa_conf: ∀h,G,L,T1,A. ⦃G, L⦄ ⊢ T1 ⁝ A →
-                    ∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → ⦃G, L⦄ ⊢ T2 ⁝ A.
+lemma cpx_aaa_conf: ∀h,G,L. Conf3 … (aaa G L) (cpx h G L).
 /2 width=6 by cpx_aaa_conf_lfpx/ qed-.
 
-lemma lfpx_aaa_conf: ∀h,G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A →
-                     ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L2⦄ ⊢ T ⁝ A.
+(* Basic_2A1: uses: lpx_aaa_conf *)
+lemma lfpx_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpx h G T).
 /2 width=6 by cpx_aaa_conf_lfpx/ qed-.