proposition: Lemma DecodeBindOpt_assoc: forall (A B C D : Type) (a_opt : option (A * B)) (f : A -> B -> option (C * B)) (g : C -> B -> option (D * B)), (`(c, b) <- (`(a, b) <- a_opt; f a b); g c b) = (`(a, b) <- a_opt; `(c, b) <- f a b; g c b).
proof: Proof. destruct a_opt as [ [? ?] | ]; simpl; intros. - destruct (f a b) as [ [? ?] | ]; reflexivity. - 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.Formats.ByteBuffer