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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma
index 30a025356..52f8e6797 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma
@@ -45,12 +45,12 @@ qed.
 lemma acle_le_monotonic_le (k1) (k2):
       k1 ≤ k2 → (ac_le k1) ⊆ (ac_le k2).
 #k1 #k2 #Hk #m #Hm
-/3 width=3 by acle_refl, transitive_le/
+/3 width=3 by acle_refl, nle_trans/
 qed.
 
 lemma acle_eq_le (k): (ac_eq k) ⊆ (ac_le k).
 #k #m #Hm destruct
-/2 width=1 by acle_refl, le_n/
+/2 width=1 by nle_refl, acle_refl/
 qed.
 
 lemma acle_le_eq (k): (ac_le k) ⊆ (ac_eq k).