milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / computation / cpxs_lreq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_lreq.ma
index 025cfdc2f3580215ed8824d6e2879b3be97849da..b110276dc9466e62a949b542fa451535b7753beb 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_lreq.ma
@@ -20,5 +20,5 @@ include "basic_2A/computation/cpxs.ma".
 (* Properties on equivalence for local environments *************************)
 
 lemma lreq_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (lreq 0 (∞)).
-/3 width=5 by lreq_cpx_trans, LTC_lsub_trans/
+/3 width=5 by lreq_cpx_trans, CTC_lsub_trans/
 qed-.