update in ground, static_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / pnat_iter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma b/matita/matita/contribs/lambdadelta/ground/arith/pnat_iter.ma
index 5361dcef37569b4d306fb6f2492e3327a7f9c00d..95425f8eb2ca97928080d872a053493b83347e95 100644 (file)
--- 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 â\89\90 f^{A}𝟏.
+lemma piter_unit (A) (f): f â\8a\9c f^{A}𝟏.
 // qed.
 
-lemma piter_succ (A) (f) (p): f â\88\98 f^p â\89\90 f^{A}(↑p).
+lemma piter_succ (A) (f) (p): f â\88\98 f^p â\8a\9c f^{A}(↑p).
 // qed.
 
 (* Advanced constructions ***************************************************)
 
-lemma piter_appl (A) (f) (p): f â\88\98 f^p â\89\90 f^{A}p ∘ f.
+lemma piter_appl (A) (f) (p): f â\88\98 f^p â\8a\9c 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 â\88\98 f â\89\90 g â\88\98 h â\86\92 h â\88\98 (f^{A}p) â\89\90 (g^{B}p) ∘ h.
+      h â\88\98 f â\8a\9c g â\88\98 h â\86\92 h â\88\98 (f^{A}p) â\8a\9c (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/