proposition: Lemma AlignedDecodeDuplicate {C D : Type} {cache : Cache} (f : ByteString -> D) (f' : forall sz, ByteBuffer.t sz -> nat -> D) (t : D -> DecodeM (C * ByteString) ByteString) (t' : D -> forall {numBytes}, AlignedDecodeM C numBytes) (f'_OK : forall sz v n, (f' (S sz) v (S n) = f' sz (Vector.tl v) n)) : (forall d, DecodeMEquivAlignedDecodeM (t d) (@t' d)) -> (forall sz v, f (build_aligned_ByteString v) = f' sz v 0) -> DecodeMEquivAlignedDecodeM (fun v cd => t (f v) v cd) (fun numBytes v0 n => (@t' (f' _ v0 n) _ v0 n)).
proof: Proof. unfold DecodeMEquivAlignedDecodeM; intros; intuition. - specialize (H (f' (S numBytes_hd) v (S n))); intuition. rewrite H1; eauto. rewrite f'_OK; eauto. - specialize (H (f b)); intuition eauto. - specialize (H (f' _ v 0)); intuition. specialize (H4 n v cd); split_and. eapply H3. rewrite H0 in H1. eauto. - specialize (H (f' _ v 0)); intuition eauto. specialize (H4 n v cd); split_and. eapply H3 in H1. rewrite H0. eauto. - specialize (H (f' _ v 0)); intuition eauto. specialize (H4 n v cd); split_and. eapply H4. rewrite H0 in H1; eauto. - specialize (H (f' _ v 0)); intuition eauto. specialize (H4 n v cd); split_and. rewrite H0 in H1; eauto. 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