X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_id_eq.ma;h=cb7ff5bf532bfb5874eb73619ee6297676e19d0e;hb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;hp=1e1fd6af594b4b21f65f844dbee799b6aa9cc9ae;hpb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;p=helm.git

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 1e1fd6af5..cb7ff5bf5 100644
--- 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 ≡ f → 𝐢 ≡ f.
+corec lemma pr_id_eq (f): ⫯f ≐ f → 𝐢 ≐ 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): 𝐢 ≡ f → ⫯f ≡ f.
+corec lemma pr_id_inv_eq (f): 𝐢 ≐ f → ⫯f ≐ f.
 cases pr_id_unfold #Hf
 cases (pr_eq_inv_push_sn … Hf) [|*: // ] #_ #H
 cases H in Hf; -H #Hf