update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isd.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isd.ma
index 1f92d0cf9a0ff4881f2477fa32fad9a019c3af5f..08f4939e840c4b28e394baabf0aa21b309c1dc37 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isd.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_isd.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_sle.ma".
 
 (*** sle_isdiv_dx *)
 corec lemma pr_sle_isd_dx:
-            â\88\80f2. ð\9d\9b\80â\9dªf2â\9d« → ∀f1. f1 ⊆ f2.
+            â\88\80f2. ð\9d\9b\80â\9d¨f2â\9d© → ∀f1. f1 ⊆ f2.
 #f2 * -f2
 #f2 #g2 #Hf2 #H2 #f1 cases (pr_map_split_tl f1) *
 /3 width=5 by pr_sle_weak, pr_sle_next/
@@ -31,7 +31,7 @@ qed.
 
 (*** sle_inv_isdiv_sn *)
 corec lemma pr_sle_inv_isd_sn:
-            â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 ð\9d\9b\80â\9dªf1â\9d« â\86\92 ð\9d\9b\80â\9dªf2â\9d«.
+            â\88\80f1,f2. f1 â\8a\86 f2 â\86\92 ð\9d\9b\80â\9d¨f1â\9d© â\86\92 ð\9d\9b\80â\9d¨f2â\9d©.
 #f1 #f2 * -f1 -f2
 #f1 #f2 #g1 #g2 #Hf * * #H
 [1,3: elim (pr_isd_inv_push … H) // ]