X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_iter.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fpnat_iter.ma;h=95425f8eb2ca97928080d872a053493b83347e95;hb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;hp=5361dcef37569b4d306fb6f2492e3327a7f9c00d;hpb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 5361dcef3..95425f8eb 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
@@ -31,22 +31,22 @@ interpretation
 
 (* Basic constructions ******************************************************)
 
-lemma piter_unit (A) (f): f ≐ f^{A}𝟏.
+lemma piter_unit (A) (f): f ⊜ f^{A}𝟏.
 // qed.
 
-lemma piter_succ (A) (f) (p): f ∘ f^p ≐ f^{A}(↑p).
+lemma piter_succ (A) (f) (p): f ∘ f^p ⊜ f^{A}(↑p).
 // qed.
 
 (* Advanced constructions ***************************************************)
 
-lemma piter_appl (A) (f) (p): f ∘ f^p ≐ f^{A}p ∘ f.
+lemma piter_appl (A) (f) (p): f ∘ f^p ⊜ f^{A}p ∘ f.
 #A #f #p elim p -p //
 #p #IH @exteq_repl
 /3 width=5 by compose_repl_fwd_dx, compose_repl_fwd_sn, exteq_canc_dx/
 qed.
 
 lemma piter_compose (A) (B) (f) (g) (h) (p):
-      h ∘ f ≐ g ∘ h → h ∘ (f^{A}p) ≐ (g^{B}p) ∘ h.
+      h ∘ f ⊜ g ∘ h → h ∘ (f^{A}p) ⊜ (g^{B}p) ∘ h.
 #A #B #f #g #h #p elim p -p
 [ #H @exteq_repl
   /2 width=5 by compose_repl_fwd_sn, compose_repl_fwd_dx/