Correctness proofs for this combinator. Correctness, termination, and ambiguity proofs for repetition.