X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Ftprs_tprs.ma;h=87a4a71abd2eb2d9c55b874f83423ef014f2441d;hb=eb4b3b1b307fc392c36f0be253e6a111553259bc;hp=ec3c9cc57e8212244682f5232457c930632ddda9;hpb=bdff98417627c404aacec8ebb07812287783c500;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
index ec3c9cc57..87a4a71ab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/tprs_tprs.ma
@@ -22,7 +22,7 @@ include "basic_2/computation/tprs.ma".
 (* Basic_1: was: pr1_strip *)
 lemma tprs_strip: ∀T1,T. T ➡* T1 → ∀T2. T ➡ T2 →
                   ∃∃T0. T1 ➡ T0 & T2 ➡* T0.
-/3 width=3/ qed.
+/3 width=3 by TC_strip1, tpr_conf/ qed.
 
 (* Main propertis ***********************************************************)