X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_sle_eq.ma;h=aa826268ead1e14fe49a7bfbc7d2341541c264cb;hb=HEAD;hp=383ad127fae9e2bf0025d060d10e79a3b4812f41;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
index 383ad127f..aa826268e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_sle_eq.ma
@@ -56,5 +56,5 @@ qed-.
 
 (*** sle_refl_eq *)
 lemma pr_sle_refl_eq:
-      ∀f1,f2. f1 ≡ f2 → f1 ⊆ f2.
+      ∀f1,f2. f1 ≐ f2 → f1 ⊆ f2.
 /2 width=3 by pr_sle_eq_repl_back_dx/ qed.