update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isf.ma
index 032774d73b3735d221d0ff060505870339fb2744..feef9f0695dec3d4f96429d96b42f67b4f135a2b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sor_isf.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sor_fcla.ma".
 
 (*** sor_isfin_ex *)
 lemma pr_sor_isf_bi:
-      â\88\80f1,f2. ð\9d\90\85â\9dªf1â\9d« â\86\92 ð\9d\90\85â\9dªf2â\9d« â\86\92 â\88\83â\88\83f. f1 â\8b\93 f2 â\89\98 f & ð\9d\90\85â\9dªfâ\9d«.
+      â\88\80f1,f2. ð\9d\90\85â\9d¨f1â\9d© â\86\92 ð\9d\90\85â\9d¨f2â\9d© â\86\92 â\88\83â\88\83f. f1 â\8b\93 f2 â\89\98 f & ð\9d\90\85â\9d¨fâ\9d©.
 #f1 #f2 * #n1 #H1 * #n2 #H2 elim (pr_sor_fcla_bi … H1 … H2) -H1 -H2
 /3 width=4 by ex2_intro, ex_intro/
 qed-.
@@ -30,14 +30,14 @@ qed-.
 
 (*** sor_fwd_isfin_sn *)
 lemma pr_sor_des_isf_sn:
-      â\88\80f. ð\9d\90\85â\9dªfâ\9d« â\86\92 â\88\80f1,f2. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9dªf1â\9d«.
+      â\88\80f. ð\9d\90\85â\9d¨fâ\9d© â\86\92 â\88\80f1,f2. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9d¨f1â\9d©.
 #f * #n #Hf #f1 #f2 #H
 elim (pr_sor_des_fcla_sn … Hf … H) -f -f2 /2 width=2 by ex_intro/
 qed-.
 
 (*** sor_fwd_isfin_dx *)
 lemma pr_sor_des_isf_dx:
-      â\88\80f. ð\9d\90\85â\9dªfâ\9d« â\86\92 â\88\80f1,f2. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9dªf2â\9d«.
+      â\88\80f. ð\9d\90\85â\9d¨fâ\9d© â\86\92 â\88\80f1,f2. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9d¨f2â\9d©.
 #f * #n #Hf #f1 #f2 #H
 elim (pr_sor_des_fcla_dx … Hf … H) -f -f1 /2 width=2 by ex_intro/
 qed-.
@@ -46,13 +46,13 @@ qed-.
 
 (*** sor_isfin *)
 lemma pr_sor_inv_isf_bi:
-      â\88\80f1,f2. ð\9d\90\85â\9dªf1â\9d« â\86\92 ð\9d\90\85â\9dªf2â\9d« â\86\92 â\88\80f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+      â\88\80f1,f2. ð\9d\90\85â\9d¨f1â\9d© â\86\92 ð\9d\90\85â\9d¨f2â\9d© â\86\92 â\88\80f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
 #f1 #f2 #Hf1 #Hf2 #f #Hf elim (pr_sor_isf_bi … Hf1 … Hf2) -Hf1 -Hf2
 /3 width=6 by pr_sor_mono, pr_isf_eq_repl_back/
 qed-.
 
 (*** sor_inv_isfin3 *)
 lemma pr_sor_inv_isf:
-      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9dªfâ\9d« →
-      â\88§â\88§ ð\9d\90\85â\9dªf1â\9d« & ð\9d\90\85â\9dªf2â\9d«.
+      â\88\80f1,f2,f. f1 â\8b\93 f2 â\89\98 f â\86\92 ð\9d\90\85â\9d¨fâ\9d© →
+      â\88§â\88§ ð\9d\90\85â\9d¨f1â\9d© & ð\9d\90\85â\9d¨f2â\9d©.
 /3 width=4 by pr_sor_des_isf_dx, pr_sor_des_isf_sn, conj/ qed-.