proposition: Lemma decode_word_plus': forall (n m : nat) (v : ByteString), decode_word' (n + m) v = (`(w, v') <- decode_word' n v; `(w', v'') <- decode_word' m v'; Some (eq_rect _ _ (Core.append_word w' w) _ (plus_comm_transparent _ _), v'')).
proof: Proof. induction n. - simpl; intros. destruct (decode_word' m v) as [ [? ?] | ]; simpl; repeat f_equal. revert w; clear. induction w; simpl; eauto. rewrite IHw at 1. rewrite Core.succ_eq_rect; f_equal. apply Eqdep_dec.UIP_dec; auto with arith. - simpl; intros. simpl; rewrite !DecodeBindOpt_assoc; destruct (ByteString_dequeue v) as [ [? ?] | ]; try reflexivity. simpl; rewrite !DecodeBindOpt_assoc. rewrite IHn. simpl; rewrite !DecodeBindOpt_assoc. destruct (decode_word' n b0) as [ [? ?] | ]; try reflexivity. simpl; rewrite !DecodeBindOpt_assoc. destruct (decode_word' m b1) as [ [? ?] | ]; try reflexivity. simpl; f_equal; f_equal; clear. revert b n w; induction w0; simpl; intros. + apply SW_word_eq_rect_eq. + erewrite !SW_word_eq_rect_eq; simpl. erewrite <- !WS_eq_rect_eq. f_equal. rewrite SW_word_append. rewrite <- Equality.transport_pp. f_equal. Unshelve. omega. omega. 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