X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Ffunctional%2Fmf_exteq.ma;h=ab162c630e532aef3716b3f47376bf4db88fe66b;hb=291fe1d3b56faf91d07099f43f3ebde2988649e1;hp=0f6975a73bad49fc6d1224bc3d760b62b91bd3cb;hpb=b5507c449ba38a76666a35664f9cf4e1953ad8ec;p=helm.git 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 0f6975a73..ab162c630 100644 --- 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 … (λgv,lv.●[gv,lv]T) (exteq …) (exteq …) (eq …). +lemma mf_comp (T): compatible_3 … (λgv,lv.■[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): ●[mf_gi,mf_li]T = T. +lemma mf_id (T): ■[mf_gi,mf_li]T = T. #T elim T -T * // [ #p #I #V #T #IHV #IHT