update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / rtmap_fcla.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
index 89460528d3684c688de3fbf66338402eee65ebc2..436b60ea30c6abd2020039ddf583fae78bf7723d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_fcla.ma
@@ -18,7 +18,7 @@ include "ground_2/relocation/rtmap_isid.ma".
 (* RELOCATION MAP ***********************************************************)
 
 inductive fcla: relation2 rtmap nat ≝
-| fcla_isid: â\88\80f. ð\9d\90\88â¦\83fâ¦\84 → fcla f 0
+| fcla_isid: â\88\80f. ð\9d\90\88â\9dªfâ\9d« → fcla f 0
 | fcla_push: ∀f,n. fcla f n → fcla (⫯f) n
 | fcla_next: ∀f,n. fcla f n → fcla (↑f) (↑n)
 .
@@ -28,13 +28,13 @@ interpretation "finite colength assignment (rtmap)"
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma fcla_inv_px: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f. ⫯f = g â\86\92 ð\9d\90\82â¦\83fâ¦\84 ≘ m.
+lemma fcla_inv_px: â\88\80g,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 fcla_isid, isid_inv_push/
 #g #m #_ #f #H elim (discr_push_next … H)
 qed-.
 
-lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 ≘ m → ∀f. ↑f = g →
-                   â\88\83â\88\83n. ð\9d\90\82â¦\83fâ¦\84 ≘ n & ↑n = m.
+lemma fcla_inv_nx: â\88\80g,m. ð\9d\90\82â\9dªgâ\9d« ≘ m → ∀f. ↑f = g →
+                   â\88\83â\88\83n. ð\9d\90\82â\9dªfâ\9d« ≘ n & ↑n = m.
 #g #m * -g -m /2 width=3 by ex2_intro/
 [ #g #Hg #f #H elim (isid_inv_next …  H) -H //
 | #g #m #_ #f #H elim (discr_next_push … H)
@@ -43,29 +43,29 @@ qed-.
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma cla_inv_nn: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 â\88\80f,n. â\86\91f = g â\86\92 â\86\91n = m â\86\92 ð\9d\90\82â¦\83fâ¦\84 ≘ n.
+lemma cla_inv_nn: â\88\80g,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 (fcla_inv_nx … H … H1) -g
 #x #Hf #H destruct //
 qed-.
 
-lemma cla_inv_np: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 ≘ m → ∀f. ↑f = g → 0 = m → ⊥.
+lemma cla_inv_np: â\88\80g,m. ð\9d\90\82â\9dªgâ\9d« ≘ m → ∀f. ↑f = g → 0 = m → ⊥.
 #g #m #H #f #H1 elim (fcla_inv_nx … H … H1) -g
 #x #_ #H1 #H2 destruct
 qed-.
 
-lemma fcla_inv_xp: â\88\80g,m. ð\9d\90\82â¦\83gâ¦\84 â\89\98 m â\86\92 0 = m â\86\92 ð\9d\90\88â¦\83gâ¦\84.
+lemma fcla_inv_xp: â\88\80g,m. ð\9d\90\82â\9dªgâ\9d« â\89\98 m â\86\92 0 = m â\86\92 ð\9d\90\88â\9dªgâ\9d«.
 #g #m #H elim H -g -m /3 width=3 by isid_push/
 #g #m #_ #_ #H destruct
 qed-.
 
-lemma fcla_inv_isid: â\88\80f,n. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n â\86\92 ð\9d\90\88â¦\83fâ¦\84 → 0 = n.
+lemma fcla_inv_isid: â\88\80f,n. ð\9d\90\82â\9dªfâ\9d« â\89\98 n â\86\92 ð\9d\90\88â\9dªfâ\9d« → 0 = n.
 #f #n #H elim H -f -n /3 width=3 by isid_inv_push/
 #f #n #_ #_ #H elim (isid_inv_next … H) -H //
 qed-.
 
 (* Main forward lemmas ******************************************************)
 
-theorem fcla_mono: â\88\80f,n1. ð\9d\90\82â¦\83fâ¦\84 â\89\98 n1 â\86\92 â\88\80n2. ð\9d\90\82â¦\83fâ¦\84 ≘ n2 → n1 = n2.
+theorem fcla_mono: â\88\80f,n1. ð\9d\90\82â\9dªfâ\9d« â\89\98 n1 â\86\92 â\88\80n2. ð\9d\90\82â\9dªfâ\9d« ≘ n2 → n1 = n2.
 #f #n #H elim H -f -n
 [ /2 width=3 by fcla_inv_isid/
 | /3 width=3 by fcla_inv_px/
@@ -76,12 +76,12 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma fcla_eq_repl_back: â\88\80n. eq_repl_back â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 ≘ n).
+lemma fcla_eq_repl_back: â\88\80n. eq_repl_back â\80¦ (λf. ð\9d\90\82â\9dªfâ\9d« ≘ n).
 #n #f1 #H elim H -f1 -n /3 width=3 by fcla_isid, isid_eq_repl_back/
 #f1 #n #_ #IH #g2 #H [ elim (eq_inv_px … H) | elim (eq_inv_nx … H) ] -H
 /3 width=3 by fcla_push, fcla_next/
 qed-.
 
-lemma fcla_eq_repl_fwd: â\88\80n. eq_repl_fwd â\80¦ (λf. ð\9d\90\82â¦\83fâ¦\84 ≘ n).
+lemma fcla_eq_repl_fwd: â\88\80n. eq_repl_fwd â\80¦ (λf. ð\9d\90\82â\9dªfâ\9d« ≘ n).
 #n @eq_repl_sym /2 width=3 by fcla_eq_repl_back/
 qed-.