- new definition of lazy equivalence for local environments,

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
index c3041b3a58a5178ea5ef98233b14c70850382e67..ef976b4add038aaa3c1db4398e2181b48b562e7d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -65,7 +65,7 @@ lemma yplus_assoc: associative … yplus.
 ]
 qed.
 
-lemma yplus_O_sn: ∀n:ynat. 0 + n = n.
+lemma yplus_O1: ∀n:ynat. 0 + n = n.
 #n >yplus_comm // qed.
 
 (* Basic inversion lemmas ***************************************************)