proposition: Lemma FindFuncBind {A C D : Type} {cache : Cache} : forall (decode_A : DecodeM (A * ByteString) ByteString) (t : A -> DecodeM (C * ByteString) ByteString) (t' : D -> A -> DecodeM (C * ByteString) ByteString) (d : D), (forall a t'' cd', (t a t'' cd') = t' d a t'' cd') -> (forall v cd, (`(a, t'', cd') <- decode_A v cd; t a t'' cd') = (`(a, t'', cd') <- decode_A v cd; t' d a t'' cd')).
proof: Proof. intros. destruct (decode_A v cd) as [ [ [? ?] ?] | ]; simpl; 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