Function dependent_ghost::proof::axiom

pub fn axiom<P>() -> Proof<P>

Define an axiom that is trivially true in an underlying theory. This will be most useful in defining domain-specific laws about the behavior of some data structure described by a ghostly type. For example, we might encode the fact that adding a key to a map leaves the other keys untouched as an axiom.