Correctness proofs for this combinator. Correctness, disjointness, and malleability proofs for alternatives.