update in ground, basic_2A and apps_2

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

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma
index 0f6975a73bad49fc6d1224bc3d760b62b91bd3cb..ab162c630e532aef3716b3f47376bf4db88fe66b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma
@@ -20,7 +20,7 @@ include "apps_2/functional/mf.ma".
 
 (* Properties with extensional equivalence **********************************)
 
-lemma mf_comp (T): compatible_3 â\80¦ (λgv,lv.â\97\8f[gv,lv]T) (exteq …) (exteq …) (eq …).
+lemma mf_comp (T): compatible_3 â\80¦ (λgv,lv.â\96 [gv,lv]T) (exteq …) (exteq …) (eq …).
 #T elim T -T *
 [ //
 | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv
@@ -36,7 +36,7 @@ qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma mf_id (T): â\97\8f[mf_gi,mf_li]T = T.
+lemma mf_id (T): â\96 [mf_gi,mf_li]T = T.
 #T elim T -T * //
 [ #p #I #V #T #IHV #IHT
   <IHV in ⊢ (???%); <IHT in ⊢ (???%); -IHV -IHT