update in ground, static_2 and apps_2

[helm.git] / matita / matita / contribs / lambdadelta / apps_2 / functional / mf_vpush_vlift.ma

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 c1f6e76ce8ff862690b87d0ec41842bf2c78572d..1155e3487f6d1cc7decb3c130110612007fe7897 100644 (file)
--- 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): â\87¡[0â\86\90â\86\91[â\86\91l,1]T]â\87¡[l]v â\89\90⇡[↑l]⇡[0←T]v.
+lemma mf_vpush_vlift_swap_O (v) (T) (l): â\87¡[0â\86\90â\86\91[â\86\91l,1]T]â\87¡[l]v â\8a\9c⇡[↑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): â\87¡[0â\86\90#0]â\87¡[l]v â\89\90⇡[↑l]⇡[0←#0]v.
+lemma mf_vpush_vlift_swap_O_lref_O (v) (l): â\87¡[0â\86\90#0]â\87¡[l]v â\8a\9c⇡[↑l]⇡[0←#0]v.
 #v #l @(mf_vpush_vlift_swap_O … (#0))
 qed.