update in ground, static_2 and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
index 855934ca218e8048728c03f49eb015fa02d7d934..ccc1c34f0147739cddd1f40d70335907efc9b78f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf_vpush.ma".
 
 (* Properties with extensional equivalence **********************************)
 
-lemma mf_lc_id: â\87¡[0â\86\90#0]mf_li â\89\90 mf_li.
+lemma mf_lc_id: â\87¡[0â\86\90#0]mf_li â\8a\9c mf_li.
 #i elim (eq_or_gt i) #Hi destruct //
 >mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
 qed.
@@ -37,7 +37,7 @@ qed-.
 (* Main properties with extensional equivalence *****************************)
 
 theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
-                       â\88\80v,T1,T2. â\87¡[l2â\86\90T2]â\87¡[l1â\86\90T1]v â\89\90 ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
+                       â\88\80v,T1,T2. â\87¡[l2â\86\90T2]â\87¡[l1â\86\90T1]v â\8a\9c ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
 #l1 #l2 #Hl21 #v #T1 #T2 #i
 elim (lt_or_eq_or_gt i l2) #Hl2 destruct
 [ lapply (lt_to_le_to_lt … Hl2 Hl21) #Hl1