- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / reducibility / tpr_tpr.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
index a50580b96236adde25bef869fc682cbed50a2e46..1522d00c0402548f2adf1506fd99c7544b2292fd 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr_tpr.ma
@@ -279,5 +279,5 @@ qed.
 (* Basic_1: was: pr0_confluence *)
 theorem tpr_conf: ∀T0:term. ∀T1,T2. T0 ➡ T1 → T0 ➡ T2 →
                   ∃∃T. T1 ➡ T & T2 ➡ T.
-#T @(tw_wf_ind … T) -T /3 width=6 by tpr_conf_aux/
+#T @(tw_ind … T) -T /3 width=6 by tpr_conf_aux/
 qed.