update in ground static_2 basic_2 apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
index 8c67bfb660dc2be95b217678fd48c48a4f813063..010fa0548896e6d0b637704780faab929c425ad4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pat_lt.ma".
 
 (*** at_eq_repl_back *)
 corec lemma pr_pat_eq_repl_back (i1) (i2):
-            pr_eq_repl_back (λf. @â\9dªi1,fâ\9d« ≘ i2).
+            pr_eq_repl_back (λf. @â\9d¨i1,fâ\9d© ≘ i2).
 #f1 * -f1 -i1 -i2
 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12
   cases (pr_eq_inv_push_sn … H12 … H) -g1 /2 width=2 by pr_pat_refl/
@@ -34,11 +34,11 @@ qed-.
 
 (*** at_eq_repl_fwd *)
 lemma pr_pat_eq_repl_fwd (i1) (i2):
-      pr_eq_repl_fwd (λf. @â\9dªi1,fâ\9d« ≘ i2).
+      pr_eq_repl_fwd (λf. @â\9d¨i1,fâ\9d© ≘ i2).
 #i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
 qed-.
 
-lemma pr_pat_eq (f): ⫯f â\89¡ f â\86\92 â\88\80i. @â\9dªi,fâ\9d« ≘ i.
+lemma pr_pat_eq (f): ⫯f â\89¡ f â\86\92 â\88\80i. @â\9d¨i,fâ\9d© ≘ i.
 #f #Hf #i elim i -i
 [ /3 width=3 by pr_pat_eq_repl_back, pr_pat_refl/
 | /3 width=7 by pr_pat_eq_repl_back, pr_pat_push/
@@ -48,7 +48,7 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 corec lemma pr_pat_inv_eq (f):
-            (â\88\80i. @â\9dªi,fâ\9d« ≘ i) → ⫯f ≡ f.
+            (â\88\80i. @â\9d¨i,fâ\9d© ≘ i) → ⫯f ≡ f.
 #Hf
 lapply (Hf (𝟏)) #H
 lapply (pr_pat_des_id … H) -H #H