Correctness proofs for this combinator. Correctness proofs for dependent formats that omit their header value.