partial commit in static_2

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

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/acle.ma
index 30a025356a5df12ed6f2d26c5a8dd1e7e0a5dca8..52f8e6797b95e45e0da620ae0b513d3aa3824d0e 100644 (file)
--- 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).