include "logic/equality.ma".
definition compose \def
\lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A.
f (g x).
include "logic/equality.ma".
definition compose \def
\lambda A,B,C:Type.\lambda f:(B\to C).\lambda g:(A\to B).\lambda x:A.
f (g x).