- lambdadelta: last recursive part of preservation finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / ssta_ltpss_sn.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma
index 342a839d52957c6fbf76868bf3d0739447548bf7..d554f1fe4dd861e0ffcb4957aee994084e8c1ec5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_ltpss_sn.ma
@@ -19,9 +19,9 @@ include "basic_2/static/ssta_ltpss_dx.ma".
 
 (* Properties about sn parallel unfold **************************************)
 
-lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g, l] U1 →
+lemma ssta_ltpss_sn_conf: ∀h,g,L1,T,U1,l. ⦃h, L1⦄ ⊢ T •[g] ⦃l, U1⦄ →
                           ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
-                          ∃∃U2. ⦃h, L2⦄ ⊢ T •[g, l] U2 & L1 ⊢ U1 ▶* [d, e] U2.
+                          ∃∃U2. ⦃h, L2⦄ ⊢ T •[g] ⦃l, U2⦄ & L1 ⊢ U1 ▶* [d, e] U2.
 #h #g #L1 #T #U1 #l #HTU1 #L2 #d #e #HL12
 lapply (ltpss_sn_ltpssa … HL12) -HL12 #HL12
 @(ltpssa_ind … HL12) -L2 [ /2 width=3/ ] -HTU1
@@ -33,10 +33,10 @@ lapply (ltpss_sn_tpss_trans_eq … HU2 … HL1) -HU2 -HL1 #HU2
 lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
 qed.
 
-lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_sn_tpss_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                                ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
                                ∀T2. L2 ⊢ T1 ▶* [d, e] T2 →
-                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+                               ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ &
                                      L1 ⊢ U1 ▶* [d, e] U2.
 #h #g #L1 #T1 #U1 #l #HTU1 #L2 #d #e #HL12 #T2 #HT12
 elim (ssta_ltpss_sn_conf … HTU1 … HL12) -HTU1 #U #HT1U #HU1
@@ -45,9 +45,9 @@ lapply (ltpss_sn_tpss_trans_eq … HU2 … HL12) -HU2 -HL12 #HU2
 lapply (tpss_trans_eq … HU1 HU2) -U /2 width=3/
 qed.
 
-lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g, l] U1 →
+lemma ssta_ltpss_sn_tps_conf: ∀h,g,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ →
                               ∀L2,d,e. L1 ⊢ ▶* [d, e] L2 →
                               ∀T2. L2 ⊢ T1 ▶ [d, e] T2 →
-                              ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g, l] U2 &
+                              ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ &
                                     L1 ⊢ U1 ▶* [d, e] U2.
 /3 width=3/ qed.