X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Fmf_vpush_vlift.ma;h=1155e3487f6d1cc7decb3c130110612007fe7897;hb=ca1807b86671236be3042b77dbc65034d0aa77c2;hp=c1f6e76ce8ff862690b87d0ec41842bf2c78572d;hpb=ea918ec7701db4458c5ca25885e80abc6fed1be7;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
index c1f6e76ce..1155e3487 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_vlift.ma
@@ -19,7 +19,7 @@ include "apps_2/functional/mf_vpush.ma".
 
 (* Properties with multiple filling lift ************************************)
 
-lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ≐⇡[↑l]⇡[0←T]v.
+lemma mf_vpush_vlift_swap_O (v) (T) (l): ⇡[0←↑[↑l,1]T]⇡[l]v ⊜⇡[↑l]⇡[0←T]v.
 #v #T #l #i
 elim (eq_or_gt i) #Hi destruct
 [ >mf_vpush_eq >mf_vlift_rw >mf_vpush_eq //
@@ -28,6 +28,6 @@ elim (eq_or_gt i) #Hi destruct
 ]
 qed.
 
-lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ≐⇡[↑l]⇡[0←#0]v.
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): ⇡[0←#0]⇡[l]v ⊜⇡[↑l]⇡[0←#0]v.
 #v #l @(mf_vpush_vlift_swap_O … (#0))
 qed.