update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
index c8e71eef9dc3a672f9ca03b6053a6fe3519e5551..7bed357e17e61ce35f9389c90529947a9542d821 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_coafter_coafter.ma".
 
 (*** coafter_isid_sn *)
 corec lemma pr_coafter_isi_sn:
-            â\88\80f1. ð\9d\90\88â\9dªf1â\9d« → ∀f2. f1 ~⊚ f2 ≘ f2.
+            â\88\80f1. ð\9d\90\88â\9d¨f1â\9d© → ∀f2. f1 ~⊚ f2 ≘ f2.
 #f1 * -f1 #f1 #g1 #Hf1 #H1 #f2
 cases (pr_map_split_tl f2) #H2
 /3 width=7 by pr_coafter_push, pr_coafter_refl/
@@ -29,7 +29,7 @@ qed.
 
 (*** coafter_isid_dx *)
 corec lemma pr_coafter_isi_dx:
-            â\88\80f2,f. ð\9d\90\88â\9dªf2â\9d« â\86\92 ð\9d\90\88â\9dªfâ\9d« → ∀f1. f1 ~⊚ f2 ≘ f.
+            â\88\80f2,f. ð\9d\90\88â\9d¨f2â\9d© â\86\92 ð\9d\90\88â\9d¨fâ\9d© → ∀f1. f1 ~⊚ f2 ≘ f.
 #f2 #f * -f2 #f2 #g2 #Hf2 #H2 * -f #f #g #Hf #H #f1
 cases (pr_map_split_tl f1) #H1
 [ /3 width=7 by pr_coafter_refl/
@@ -41,10 +41,10 @@ qed.
 
 (*** coafter_isid_inv_sn *)
 lemma pr_coafter_isi_inv_sn:
-      â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªf1â\9d« → f2 ≡ f.
+      â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© → f2 ≡ f.
 /3 width=6 by pr_coafter_isi_sn, pr_coafter_mono/ qed-.
 
 (*** coafter_isid_inv_dx *)
 lemma pr_coafter_isi_inv_dx:
-      â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªf2â\9d« â\86\92 ð\9d\90\88â\9dªfâ\9d«.
+      â\88\80f1,f2,f. f1 ~â\8a\9a f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 ð\9d\90\88â\9d¨fâ\9d©.
 /4 width=4 by pr_eq_id_isi, pr_coafter_isi_dx, pr_coafter_mono/ qed-.