the theory of extended multiple substitution for therms is complete

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
index efa8e3da6222e0c435c61d1c72b837b4b8025a6d..640f4dbfce2192b8a6a3feb6ef0dd923f875aeaf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs.ma
@@ -60,7 +60,7 @@ lemma cprs_strap2: ∀G,L,T1,T,T2.
 normalize /2 width=3/ qed.
 
 lemma lsubr_cprs_trans: ∀G. lsub_trans … (cprs G) lsubr.
-/3 width=5 by lsubr_cpr_trans, TC_lsub_trans/
+/3 width=5 by lsubr_cpr_trans, LTC_lsub_trans/
 qed-.
 
 (* Basic_1: was: pr3_pr1 *)