update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla.ma
index 54c81af81afdf29e07dbf3271f4b2042dc81dd24..d0a9216b49f306ea12e8f9a53fa3ac29ef5971ef 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_fcla.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_isi.ma".
 (*** fcla *)
 inductive pr_fcla: relation2 pr_map nat ≝
 (*** fcla_isid *)
-| pr_fcla_isi (f): ð\9d\90\88â\9dªfâ\9d« → pr_fcla f (𝟎)
+| pr_fcla_isi (f): ð\9d\90\88â\9d¨fâ\9d© → pr_fcla f (𝟎)
 (*** fcla_push *)
 | pr_fcla_push (f) (n): pr_fcla f n → pr_fcla (⫯f) n
 (*** fcla_next *)
@@ -35,7 +35,7 @@ interpretation
 (* Basic inversions *********************************************************)
 
 (*** fcla_inv_px *)
-lemma pr_fcla_inv_push (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ m.
+lemma pr_fcla_inv_push (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ m.
 #g #m * -g -m
 [ /3 width=3 by pr_fcla_isi, pr_isi_inv_push/
 | #g #m #Hg #f #H >(eq_inv_pr_push_bi … H) -f //
@@ -44,7 +44,7 @@ lemma pr_fcla_inv_push (g) (m): 𝐂❪g❫ ≘ m → ∀f. ⫯f = g → 𝐂❪
 qed-.
 
 (*** fcla_inv_nx *)
-lemma pr_fcla_inv_next (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f. â\86\91f = g â\86\92 â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & ↑n = m.
+lemma pr_fcla_inv_next (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f. â\86\91f = g â\86\92 â\88\83â\88\83n. ð\9d\90\82â\9d¨fâ\9d© ≘ n & ↑n = m.
 #g #m * -g -m
 [ #g #Hg #f #H destruct
   elim (pr_isi_inv_next … Hg) -Hg //
@@ -57,25 +57,25 @@ qed-.
 (* Advanced inversions ******************************************************)
 
 (*** cla_inv_nn *)
-lemma pr_cla_inv_next_succ (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â\9dªfâ\9d« ≘ n.
+lemma pr_cla_inv_next_succ (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â\9d¨fâ\9d© ≘ n.
 #g #m #H #f #n #H1 #H2 elim (pr_fcla_inv_next … H … H1) -g
 #x #Hf #H destruct <(eq_inv_nsucc_bi … H) -n //
 qed-.
 
 (*** cla_inv_np *)
-lemma pr_cla_inv_next_zero (g) (m): ð\9d\90\82â\9dªgâ\9d« ≘ m → ∀f. ↑f = g → 𝟎 = m → ⊥.
+lemma pr_cla_inv_next_zero (g) (m): ð\9d\90\82â\9d¨gâ\9d© ≘ m → ∀f. ↑f = g → 𝟎 = m → ⊥.
 #g #m #H #f #H1 elim (pr_fcla_inv_next … H … H1) -g
 #x #_ #H1 #H2 destruct /2 width=2 by eq_inv_zero_nsucc/
 qed-.
 
 (*** fcla_inv_xp *)
-lemma pr_fcla_inv_zero (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 ð\9d\9f\8e = m â\86\92 ð\9d\90\88â\9dªgâ\9d«.
+lemma pr_fcla_inv_zero (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 ð\9d\9f\8e = m â\86\92 ð\9d\90\88â\9d¨gâ\9d©.
 #g #m #H elim H -g -m /3 width=3 by pr_isi_push/
 #g #m #_ #_ #H destruct elim (eq_inv_zero_nsucc … H)
 qed-.
 
 (*** fcla_inv_isid *)
-lemma pr_fcla_inv_isi (g) (m): ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 ð\9d\90\88â\9dªgâ\9d« → 𝟎 = m.
+lemma pr_fcla_inv_isi (g) (m): ð\9d\90\82â\9d¨gâ\9d© â\89\98 m â\86\92 ð\9d\90\88â\9d¨gâ\9d© → 𝟎 = m.
 #f #n #H elim H -f -n /3 width=3 by pr_isi_inv_push/
 #f #n #_ #_ #H elim (pr_isi_inv_next … H) -H //
 qed-.