update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
index 8cd1873783e6159114f49923d2612a4603e8487f..bc307df7e0994735dbe7b5f4bc04fd454e3ce226 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isi.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_sor_sor.ma".
 
 (*** sor_isid_sn *)
 corec lemma pr_sor_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)
 /3 width=7 by pr_sor_push_bi, pr_sor_push_next/
@@ -30,7 +30,7 @@ qed.
 
 (*** sor_isid_dx *)
 corec lemma pr_sor_isi_dx:
-            â\88\80f2. ð\9d\90\88â\9dªf2â\9d« → ∀f1. f1 ⋓ f2 ≘ f1.
+            â\88\80f2. ð\9d\90\88â\9d¨f2â\9d© → ∀f1. f1 ⋓ f2 ≘ f1.
 #f2 * -f2
 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1)
 /3 width=7 by pr_sor_push_bi, pr_sor_next_push/
@@ -38,7 +38,7 @@ qed.
 
 (*** sor_isid *)
 lemma pr_sor_isi_bi_isi:
-      â\88\80f1,f2,f. ð\9d\90\88â\9dªf1â\9d« â\86\92 ð\9d\90\88â\9dªf2â\9d« â\86\92 ð\9d\90\88â\9dªfâ\9d« → f1 ⋓ f2 ≘ f.
+      â\88\80f1,f2,f. ð\9d\90\88â\9d¨f1â\9d© â\86\92 ð\9d\90\88â\9d¨f2â\9d© â\86\92 ð\9d\90\88â\9d¨fâ\9d© → f1 ⋓ f2 ≘ f.
 /4 width=3 by pr_sor_eq_repl_back_dx, pr_sor_eq_repl_back_sn, pr_isi_inv_eq_repl/ qed.
 
 
@@ -46,7 +46,7 @@ lemma pr_sor_isi_bi_isi:
 
 (*** sor_fwd_isid1 *)
 corec lemma pr_sor_des_isi_sn:
-            â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªf1â\9d«.
+            â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\88â\9d¨f1â\9d©.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
 [ /4 width=6 by pr_isi_inv_push, pr_isi_push/ ]
@@ -55,7 +55,7 @@ qed-.
 
 (*** sor_fwd_isid2 *)
 corec lemma pr_sor_des_isi_dx:
-            â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\88â\9dªf2â\9d«.
+            â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\88â\9d¨f2â\9d©.
 #f1 #f2 #f * -f1 -f2 -f
 #f1 #f2 #f #g1 #g2 #g #Hf #H1 #H2 #H #Hg
 [ /4 width=6 by pr_isi_inv_push, pr_isi_push/ ]
@@ -66,18 +66,18 @@ qed-.
 
 (*** sor_isid_inv_sn *)
 lemma pr_sor_inv_isi_sn:
-      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªf1â\9d« → f2 ≡ f.
+      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f1â\9d© → f2 ≡ f.
 /3 width=4 by pr_sor_isi_sn, pr_sor_mono/
 qed-.
 
 (*** sor_isid_inv_dx *)
 lemma pr_sor_inv_isi_dx:
-      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªf2â\9d« → f1 ≡ f.
+      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨f2â\9d© → f1 ≡ f.
 /3 width=4 by pr_sor_isi_dx, pr_sor_mono/
 qed-.
 
 (*** sor_inv_isid3 *)
 lemma pr_sor_inv_isi:
-      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9dªfâ\9d« →
-      â\88§â\88§ ð\9d\90\88â\9dªf1â\9d« & ð\9d\90\88â\9dªf2â\9d«.
+      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\88â\9d¨fâ\9d© →
+      â\88§â\88§ ð\9d\90\88â\9d¨f1â\9d© & ð\9d\90\88â\9d¨f2â\9d©.
 /3 width=4 by pr_sor_des_isi_dx, pr_sor_des_isi_sn, conj/ qed-.