X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN%2Falgebra%2FSetoidFun.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN%2Falgebra%2FSetoidFun.ma;h=96a583cfa94dd903c80fcbef25badd1c438849bc;hb=33e397c66c8ab7ff1adbffa6e3b2d152dbecad26;hp=4a7fde036e114a5f0482e3da0c5383f7f8aea022;hpb=e1d918026477892040e0eeb532c017153a6e1880;p=helm.git diff --git a/helm/software/matita/contribs/CoRN/algebra/SetoidFun.ma b/helm/software/matita/contribs/CoRN/algebra/SetoidFun.ma index 4a7fde036..96a583cfa 100644 --- a/helm/software/matita/contribs/CoRN/algebra/SetoidFun.ma +++ b/helm/software/matita/contribs/CoRN/algebra/SetoidFun.ma @@ -15,7 +15,7 @@ (* $Id: CSetoidFun.v,v 1.12 2004/09/22 11:06:10 loeb Exp $ *) set "baseuri" "cic:/matita/algebra/CoRN/SetoidFun". -include "Setoids.ma". +include "algebra/Setoids.ma". definition ap_fun : \forall A,B : CSetoid. \forall f,g : CSetoid_fun A B. Prop \def