proposition: Lemma AlignedDecodeBindDuplicate {A C D : Type} {cache : Cache} (decode_A : DecodeM (A * ByteString) ByteString) (f : ByteString -> D) (f' : forall sz, ByteBuffer.t sz -> nat -> D) (t : D -> A -> DecodeM (C * ByteString) ByteString) (t' : D -> forall {numBytes}, AlignedDecodeM C numBytes) (t'' : DecodeM (C * ByteString) ByteString) : (forall v cd, (`(a, t'', cd') <- decode_A v cd; t (f v) a t'' cd') = t'' v cd) -> (forall d, DecodeMEquivAlignedDecodeM (fun v cd => `(a, t'', cd') <- decode_A v cd; t d a t'' cd') (@t' d)) -> (forall sz v, f (build_aligned_ByteString v) = f' sz v 0) -> (forall sz v idx, f' (S sz) v (S idx) = f' sz (Vector.tl v) idx) -> DecodeMEquivAlignedDecodeM t'' (fun numBytes v0 idx => (@t' (f' _ v0 idx) _ v0 idx)).
proof: Proof. intros. eapply DecodeMEquivAlignedDecodeM_trans. eapply AlignedDecodeDuplicate with (t0 := fun b (v : ByteString) (cd : CacheDecode) => `(a, t'', cd') <- decode_A v cd; t b a t'' cd'); eauto. intros; simpl; apply H. intros; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.BinLib.AlignedByteString