update in ground, static_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
index c048ec4021bd49f3134b8cc81c0a4473338581e5..741da1062ed8df4106bcbf901d8778d72b8bb420 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after.ma
@@ -74,7 +74,7 @@ qed-.
 
 (*** after_mono *)
 corec theorem pr_after_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_after_inv_push_bi … Hy … H1 H2) -g1 -g2 /3 width=8 by pr_eq_push/
@@ -86,5 +86,5 @@ qed-.
 (*** after_mono_eq *)
 lemma pr_after_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_after_mono, pr_after_eq_repl_back_dx, pr_after_eq_repl_back_sn/ qed-.