- lambdadelta: first recursive part of preservation finally proved!

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma
index b094e66c1886ba52419479a76acc097e80662b75..22f09eda00a7a3fb5752ec1d6d1055774a9ec718 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs.ma
@@ -43,6 +43,9 @@ qed-.
 lemma tprs_refl: reflexive … tprs.
 /2 width=1/ qed.
 
+lemma tpr_tprs: ∀T1,T2. T1 ➡ T2 → T2 ➡* T2.
+/2 width=1/ qed.
+
 lemma tprs_strap1: ∀T1,T,T2. T1 ➡* T → T ➡ T2 → T1 ➡* T2.
 /2 width=3/ qed.