update in ground, static_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / pr_coafter_coafter.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
index 8ac9736a70378ee2f3374a99db5385c7bcf5b6df..ff06a8c3570346c3cd5e9d7ae477a3ee861b2d8c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_coafter_eq.ma".
 
 (*** coafter_mono *)
 corec theorem pr_coafter_mono:
-              â\88\80f1,f2,x,y. f1 ~â\8a\9a f2 â\89\98 x â\86\92 f1 ~â\8a\9a f2 â\89\98 y â\86\92 x â\89¡ y.
+              â\88\80f1,f2,x,y. f1 ~â\8a\9a f2 â\89\98 x â\86\92 f1 ~â\8a\9a f2 â\89\98 y â\86\92 x â\89\90 y.
 #f1 #f2 #x #y * -f1 -f2 -x
 #f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
 [ cases (pr_coafter_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -32,5 +32,5 @@ qed-.
 (*** coafter_mono_eq *)
 lemma pr_coafter_mono_eq:
       ∀f1,f2,f. f1 ~⊚ f2 ≘ f → ∀g1,g2,g. g1 ~⊚ g2 ≘ g →
-      f1 â\89¡ g1 â\86\92 f2 â\89¡ g2 â\86\92 f â\89¡ g.
+      f1 â\89\90 g1 â\86\92 f2 â\89\90 g2 â\86\92 f â\89\90 g.
 /4 width=4 by pr_coafter_mono, pr_coafter_eq_repl_back_dx, pr_coafter_eq_repl_back_sn/ qed-.