update in ground, static_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
index 1e1fd6af594b4b21f65f844dbee799b6aa9cc9ae..cb7ff5bf532bfb5874eb73619ee6297676e19d0e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_id_eq.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_id.ma".
 
 (* Constructions with pr_eq *************************************************)
 
-corec lemma pr_id_eq (f): ⫯f â\89¡ f â\86\92 ð\9d\90¢ â\89¡ f.
+corec lemma pr_id_eq (f): ⫯f â\89\90 f â\86\92 ð\9d\90¢ â\89\90 f.
 cases pr_id_unfold #Hf
 cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
 cases H in Hf; -H #Hf
@@ -30,7 +30,7 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 (* Note: this has the same proof of the previous *)
-corec lemma pr_id_inv_eq (f): ð\9d\90¢ â\89¡ f â\86\92 ⫯f â\89¡ f.
+corec lemma pr_id_inv_eq (f): ð\9d\90¢ â\89\90 f â\86\92 ⫯f â\89\90 f.
 cases pr_id_unfold #Hf
 cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
 cases H in Hf; -H #Hf