- new definition of lazy equivalence for local environments,

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_lt.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
index 6cc21d5bcc60bf6018944835931c20bcfae660df..d30d6229dc48890aa90588d1a753494eb1e21d84 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_lt.ma
@@ -98,7 +98,7 @@ lemma ylt_fwd_succ2: ∀m,n. m < ⫯n → m ≤ n.
 
 (* inversion and forward lemmas on yle **************************************)
 
-lemma lt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n.
+lemma ylt_fwd_le: ∀m:ynat. ∀n:ynat. m < n → m ≤ n.
 #m #n * -m -n /3 width=1 by yle_pred_sn, yle_inj, yle_Y/
 qed-.