update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
index f8a94240950aceeb2cfacad81bacbae709b6fa87..b1e4650b96ec53c686334a42f3ad0f8e7f1d4c5e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sdj_isi.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sdj.ma".
 
 (*** sdj_isid_dx *)
 corec lemma pr_sdj_isi_dx:
-            â\88\80f2. ð\9d\90\88â\9dªf2â\9d« → ∀f1. f1 ∥ f2.
+            â\88\80f2. ð\9d\90\88â\9d¨f2â\9d© → ∀f1. f1 ∥ f2.
 #f2 * -f2
 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1) *
 /3 width=5 by pr_sdj_next_push, pr_sdj_push_bi/
@@ -29,7 +29,7 @@ qed.
 
 (*** sdj_isid_sn *)
 corec lemma pr_sdj_isi_sn:
-            â\88\80f1. ð\9d\90\88â\9dªf1â\9d« → ∀f2. f1 ∥ f2.
+            â\88\80f1. ð\9d\90\88â\9d¨f1â\9d© → ∀f2. f1 ∥ f2.
 #f1 * -f1
 #f1 #g1 #Hf1 #H1 #f2 cases (pr_map_split_tl f2) *
 /3 width=5 by pr_sdj_push_next, pr_sdj_push_bi/
@@ -39,7 +39,7 @@ qed.
 
 (*** sdj_inv_refl *)
 corec lemma pr_sdj_inv_refl:
-            â\88\80f. f â\88¥ f â\86\92  ð\9d\90\88â\9dªfâ\9d«.
+            â\88\80f. f â\88¥ f â\86\92  ð\9d\90\88â\9d¨fâ\9d©.
 #f cases (pr_map_split_tl f) #Hf #H
 [ lapply (pr_sdj_inv_push_bi … H … Hf Hf) -H /3 width=3 by pr_isi_push/
 | elim (pr_sdj_inv_next_bi … H … Hf Hf)