- parallel substitution reaxiomatized

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

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 ec3c9cc57e8212244682f5232457c930632ddda9..87a4a71abd2eb2d9c55b874f83423ef014f2441d 100644 (file)
--- 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 ***********************************************************)