Correctness proofs for this combinator. Correctness proofs for predicates, refinements, and constants.