proposition: Lemma format_word_S {n} : forall (w : word (S n)) (bs : B), encode_word' (S n) w bs = encode_word' n (word_split_tl w) (enqueue_opt (word_split_hd w) bs).
proof: Proof. intros; pose proof (shatter_word_S w); destruct_ex; subst. simpl. clear; revert x; induction x0; simpl; intros. - simpl; reflexivity. - rewrite IHx0. reflexivity. 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