proposition: Lemma aligned_format_char_eq : forall (w : word 8) cd, refine (format_word (monoidUnit := ByteString_QueueMonoidOpt) w cd) (ret (build_aligned_ByteString (Vector.cons _ w _ (Vector.nil _)), addE cd 8)).
proof: Proof. intros; shatter_word w; simpl. unfold format_word; simpl. compute. intros. computes_to_inv; subst. match goal with |- computes_to (ret ?c) ?v => replace c with v end. computes_to_econstructor. f_equal. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _). rewrite <- !Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. unfold ByteBuffer.t; erewrite eq_rect_Vector_cons; repeat f_equal. instantiate (1 := eq_refl _); reflexivity. Unshelve. 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 Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignedDecodeMonad