update in ground, static_2 and apps_2

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

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 d7d6211ecb5d2b82f478572027a9cb23dd0ef476..2e0249286e0d1f17b6db8a3199079ee877e5cddd 100644 (file)
--- 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: â\88\80j. â\87¡[j]mf_gi â\89\90 mf_gi.
+lemma mf_gc_id: â\88\80j. â\87¡[j]mf_gi â\8a\9c 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: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\89\90 ⇡[↑l1]⇡[l2]v.
+theorem mf_vlift_swap: â\88\80l1,l2. l2 â\89¤ l1 â\86\92 â\88\80v. â\87¡[l2]â\87¡[l1]v â\8a\9c ⇡[↑l1]⇡[l2]v.
 /2 width=1 by flifts_basic_swap/ qed-.