update in ground, static_2 and 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 010fa0548896e6d0b637704780faab929c425ad4..29620d121db2173d3a988b69c325a22b72e047b4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
@@ -38,7 +38,7 @@ lemma pr_pat_eq_repl_fwd (i1) (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 → ∀i. @❨i,f❩ ≘ i.
+lemma pr_pat_eq (f): ⫯f â\89\90 f → ∀i. @❨i,f❩ ≘ 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© â\89\98 i) â\86\92 ⫯f â\89¡ f.
+            (â\88\80i. @â\9d¨i,fâ\9d© â\89\98 i) â\86\92 ⫯f â\89\90 f.
 #Hf
 lapply (Hf (𝟏)) #H
 lapply (pr_pat_des_id … H) -H #H