save before clean slate

An attempt at writing the relations algorithmically quickly confirmed
they are too complex (and interdependent) for Coq to reason about the
termination of (and using “Program Fixpoint” is not allowed on mutually
dependent functions).

This led to the decision to use a purely Prop based representation…
which then led to the realization that we needed explicit Props and
Non-Props in order to assert the negation of a property within the
definitions (since they are mutually recursive and cannot negate one
another during their definitions).

After this is defined, we will want to verify, for instance, that
Subtype and NotSubtype are intact disjoint relations on types. With the
logic simplified, hopefully this will not be too difficult.