- lambdadelta: first recursive part of preservation finally proved!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / tpss.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index cc5be0ecab230655c2413f42211b41c8f6201057..faafb36d16c422160bdb680be2736d2f7d3f872f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -40,6 +40,9 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma tps_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+/2 width=1/ qed.
+
 lemma tpss_strap1: ∀L,T1,T,T2,d,e.
                    L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. 
 /2 width=3/ qed.