- lambdadelta: last recursive part of preservation finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / dxprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
index 90663d932245da2bf079c7b6364c98b29bff8a29..4656a1595f6a8faf02e650f67664d5ffb332862f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/dxprs.ma
@@ -40,6 +40,6 @@ lemma dxprs_strap1: ∀h,g,L,T1,T,T2.
 qed.
 
 lemma dxprs_strap2: ∀h,g,L,T1,T,T2,l.
-                    ⦃h, L⦄ ⊢ T1 •[g, l+1] T → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
+                    ⦃h, L⦄ ⊢ T1 •[g] ⦃l+1, T⦄ → ⦃h, L⦄ ⊢ T •*➡*[g] T2 → ⦃h, L⦄ ⊢ T1 •*➡*[g] T2.
 #h #g #L #T1 #T #T2 #l #HT1 * /3 width=4/
 qed.