X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat_iter.ma;h=fc824317ab5e517f08f63f73c9945ef5528dfac3;hb=775ab35f714568dfcd672f0dd53a00e1ba7382cd;hp=6adaa148a3872d09a8bce16422c136591a336178;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
index 6adaa148a..fc824317a 100644
--- a/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/arith/nat_iter.ma
@@ -35,20 +35,20 @@ interpretation
 lemma niter_zero (A) (f) (a): a = (f^{A}𝟎) a.
 // qed.
 
-lemma niter_inj (A) (f) (p): f^p ≐ f^{A}(ninj p).
+lemma niter_inj (A) (f) (p): f^p ⊜ f^{A}(ninj p).
 // qed.
 
 (* Advanced constructions ***************************************************)
 
 (*** iter_n_Sm *)
-lemma niter_appl (A) (f) (n): f ∘ f^n ≐ f^{A}n ∘ f.
+lemma niter_appl (A) (f) (n): f ∘ f^n ⊜ f^{A}n ∘ f.
 #A #f * //
 #p @exteq_repl
 /2 width=5 by piter_appl, compose_repl_fwd_dx/
 qed.
 
 lemma niter_compose (A) (B) (f) (g) (h) (n):
-      h ∘ f ≐ g ∘ h → h ∘ (f^{A}n) ≐ (g^{B}n) ∘ h.
+      h ∘ f ⊜ g ∘ h → h ∘ (f^{A}n) ⊜ (g^{B}n) ∘ h.
 #A #B #f #g #h * //
 #p #H @exteq_repl
 /2 width=5 by piter_compose, compose_repl_fwd_dx/