Correctness proofs for this combinator. Correctness proofs for sequential formats discarding their suffix.