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