milestone update in ground_2 and basic_2A

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

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
index 07fed2a507ba2d1bb940e3dfc7362b5a6748bb92..b64e388773f454ea8e13fc3b7bf131625c323c3f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_pred.ma
@@ -18,24 +18,24 @@ include "ground_2/ynat/ynat.ma".
 
 (* the predecessor function *)
 definition ypred: ynat → ynat ≝ λm. match m with
-[ yinj m â\87\92 â«°m
+[ yinj m â\87\92 â\86\93m
 | Y      ⇒ Y
 ].
 
-interpretation "ynat predecessor" 'Predecessor m = (ypred m).
+interpretation "ynat predecessor" 'DownArrow m = (ypred m).
 
-lemma ypred_O: â«°(yinj 0) = yinj 0.
+lemma ypred_O: â\86\93(yinj 0) = yinj 0.
 // qed.
 
-lemma ypred_S: â\88\80m:nat. â«°(⫯m) = yinj m.
+lemma ypred_S: â\88\80m:nat. â\86\93(â\86\91m) = yinj m.
 // qed.
 
-lemma ypred_Y: (â«°∞) = ∞.
+lemma ypred_Y: (â\86\93∞) = ∞.
 // qed.
 
 (* Inversion lemmas *********************************************************)
 
-lemma ypred_inv_refl: â\88\80m:ynat. â«°m = m → m = 0 ∨ m = ∞.
+lemma ypred_inv_refl: â\88\80m:ynat. â\86\93m = m → m = 0 ∨ m = ∞.
 * // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-/4 width=1 by pred_inv_refl, or_introl, eq_f/
+/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
 qed-.