X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Facle_acle.ma;h=2edee6e4cb75a0638bca51e2fbee9d8eb718c4f7;hp=9b8998900b22a2aa3a213f285c5e2ef26fa3b346;hb=98e786e1a6bd7b621e37ba7cd4098d4a0a6f8278;hpb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma
index 9b8998900..2edee6e4c 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle_acle.ma
@@ -22,5 +22,5 @@ theorem acle_trans: Transitive … acle.
 #a1 #a #Ha1 #a2 #Ha2 #m1 #Hm1
 elim (Ha1 … Hm1) -Ha1 -Hm1 #m #Ha #Hm1
 elim (Ha2 … Ha) -Ha2 -Ha #m2 #Ha2 #Hm2
-/3 width=5 by transitive_le, ex2_intro/
+/3 width=5 by nle_trans, ex2_intro/
 qed-.