proposition: Lemma decode_unused_word_plus': forall (n m : nat) (v : ByteString), decode_unused_word' (n + m) v = (`(w, v') <- decode_unused_word' n v; `(w', v'') <- decode_unused_word' m v'; Some ((), v'')).
proof: Proof. induction n. - unfold plus; simpl; intros. destruct (decode_unused_word' m v) as [ [? ?] | ]; simpl; repeat f_equal. destruct u; eauto. - simpl; intros. unfold decode_unused_word' in *; simpl. fold plus. destruct (ByteString_dequeue v) as [ [? ?] | ]; try reflexivity. simpl. pose proof (IHn m b0). destruct (WordOpt.monoid_dequeue_word (n + m) b0) as [ [? ?] | ]; simpl in *; try congruence. simpl in *. destruct (WordOpt.monoid_dequeue_word n b0) as [ [? ?] | ]; simpl in *; try congruence. destruct (WordOpt.monoid_dequeue_word n b0) as [ [? ?] | ]; simpl in *; try congruence. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Logic.Eqdep_dec Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Sequence Fiat.Narcissus.BaseFormats Fiat.Narcissus.BinLib.AlignedEncodeMonad Coq.Vectors.Vector Coq.ZArith.ZArith Bedrock.Word Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad