X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Fmf_vlift_exteq.ma;h=2e0249286e0d1f17b6db8a3199079ee877e5cddd;hb=873fb39bdd21aa14877bf5d50db26e3a050c6d43;hp=d7d6211ecb5d2b82f478572027a9cb23dd0ef476;hpb=503500ff9a6d9cca363a42b5fe7f3f5de69239f9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
index d7d6211ec..2e0249286 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vlift_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vlift.ma".
 
 (* Properties with extensional equivalence **********************************)
 
-lemma mf_gc_id: ∀j. ⇡[j]mf_gi ≐ mf_gi.
+lemma mf_gc_id: ∀j. ⇡[j]mf_gi ⊜ mf_gi.
 // qed.
 
 lemma mf_vlift_comp (l): compatible_2 … (mf_vlift l) (exteq …) (exteq …).
@@ -30,5 +30,5 @@ qed.
 
 (* Main properties with extensional equivalence *****************************)
 
-theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ≐ ⇡[↑l1]⇡[l2]v.
+theorem mf_vlift_swap: ∀l1,l2. l2 ≤ l1 → ∀v. ⇡[l2]⇡[l1]v ⊜ ⇡[↑l1]⇡[l2]v.
 /2 width=1 by flifts_basic_swap/ qed-.