abstract Math = { cat Prop ; Elem ; fun And : Prop -> Prop -> Prop ; Even : Elem -> Prop ; Odd : Elem -> Prop ; Zero : Elem ; }