- 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 2322445109732882f9659baaded29f9a4d754f3c..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,12 +22,12 @@ 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 ***********************************************************)
 
 (* Basic_1: was: pr1_confluence *)
-theorem tprs_conf: Confluent … tprs.
+theorem tprs_conf: confluent … tprs.
 /3 width=3/ qed.
 
 (* Basic_1: was: pr1_t *)