update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isf.ma
index 3a68c00f52f27994028847416d4c1cdbc636109e..df5343cb88ec2c0aa00f90115807c25b4a1621d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isf.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_fcla.ma".
 
 (*** isfin *)
 definition pr_isf: predicate pr_map ≝
-           λf. â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n.
+           λf. â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n.
 
 interpretation
   "finite colength condition (partial relocation maps)"
@@ -29,10 +29,10 @@ interpretation
 
 (*** isfin_ind *)
 lemma pr_isf_ind (Q:predicate …):
-      (â\88\80f.  ð\9d\90\88â\9dªfâ\9d« → Q f) →
-      (â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f → Q (⫯f)) →
-      (â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f → Q (↑f)) →
-      â\88\80f. ð\9d\90\85â\9dªfâ\9d« → Q f.
+      (â\88\80f.  ð\9d\90\88â\9d¨fâ\9d© → Q f) →
+      (â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f → Q (⫯f)) →
+      (â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f → Q (↑f)) →
+      â\88\80f. ð\9d\90\85â\9d¨fâ\9d© → Q f.
 #Q #IH1 #IH2 #IH3 #f #H elim H -H
 #n #H elim H -f -n /3 width=2 by ex_intro/
 qed-.
@@ -40,12 +40,12 @@ qed-.
 (* Basic inversions *********************************************************)
 
 (*** isfin_inv_push *)
-lemma pr_isf_inv_push (g): ð\9d\90\85â\9dªgâ\9d« â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_inv_push (g): ð\9d\90\85â\9d¨gâ\9d© â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
 #g * /3 width=4 by pr_fcla_inv_push, ex_intro/
 qed-.
 
 (*** isfin_inv_next *)
-lemma pr_isf_inv_next (g): ð\9d\90\85â\9dªgâ\9d« â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_inv_next (g): ð\9d\90\85â\9d¨gâ\9d© â\86\92 â\88\80f. â\86\91f = g â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
 #g * #n #H #f #H0 elim (pr_fcla_inv_next … H … H0) -g
 /2 width=2 by ex_intro/
 qed-.
@@ -53,15 +53,15 @@ qed-.
 (* Basic constructions ******************************************************)
 
 (*** isfin_isid *)
-lemma pr_isf_isi (f): ð\9d\90\88â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªfâ\9d«.
+lemma pr_isf_isi (f): ð\9d\90\88â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨fâ\9d©.
 /3 width=2 by pr_fcla_isi, ex_intro/ qed.
 
 (*** isfin_push *)
-lemma pr_isf_push (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ«¯fâ\9d«.
+lemma pr_isf_push (f): ð\9d\90\85â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨â«¯fâ\9d©.
 #f * /3 width=2 by pr_fcla_push, ex_intro/
 qed.
 
 (*** isfin_next *)
-lemma pr_isf_next (f): ð\9d\90\85â\9dªfâ\9d« â\86\92 ð\9d\90\85â\9dªâ\86\91fâ\9d«.
+lemma pr_isf_next (f): ð\9d\90\85â\9d¨fâ\9d© â\86\92 ð\9d\90\85â\9d¨â\86\91fâ\9d©.
 #f * /3 width=2 by pr_fcla_next, ex_intro/
 qed.