Added an axiomatic definition of pure predicates. I'm not quite sure how
this will work out. It may be a bad idea depending slightly on how Coq
handles Inductive type classes.