update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isu.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isu.ma
index 311ba5542b2274c0220fec54a5a9615b444ecf0c..c4109ea8a2dc0fd5549a8ec4726eee15cc442f52 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isu.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_isu.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_after_uni.ma".
 
 (*** after_isid_isuni *)
 lemma pr_after_isu_isi_next:
-      â\88\80f1,f2. ð\9d\90\88â\9dªf2â\9d« â\86\92 ð\9d\90\94â\9dªf1â\9d« → f1 ⊚ ↑f2 ≘ ↑f1.
+      â\88\80f1,f2. ð\9d\90\88â\9d¨f2â\9d© â\86\92 ð\9d\90\94â\9d¨f1â\9d© → f1 ⊚ ↑f2 ≘ ↑f1.
 #f1 #f2 #Hf2 #H
 elim (pr_isu_inv_uni … H) -H #h #H
 /5 width=7 by pr_after_uni_isi_next, pr_after_eq_repl_back, pr_after_eq_repl_back_sn, pr_eq_next/
@@ -29,7 +29,7 @@ qed.
 
 (*** after_uni_next2 *)
 lemma pr_after_isu_next_sn:
-      â\88\80f2. ð\9d\90\94â\9dªf2â\9d« → ∀f1,f. ↑f2 ⊚ f1 ≘ f → f2 ⊚ ↑f1 ≘ f.
+      â\88\80f2. ð\9d\90\94â\9d¨f2â\9d© → ∀f1,f. ↑f2 ⊚ f1 ≘ f → f2 ⊚ ↑f1 ≘ f.
 #f2 #H #f1 #f #Hf
 elim (pr_isu_inv_uni … H) -H #h #H
 /5 width=7 by pr_after_uni_next_sn, pr_after_eq_repl_fwd_sn, pr_after_eq_repl_back_sn, pr_eq_next/