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