let Eq (a : *) : * = a -> a -> ./Bool
in  Eq