partial commit in static_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / syntax / acle_acle.ma

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 9b8998900b22a2aa3a213f285c5e2ef26fa3b346..2edee6e4cb75a0638bca51e2fbee9d8eb718c4f7 100644 (file)
--- 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-.