proposition: Lemma AlignedFormatChar {numBytes} : forall (w : word 8) ce ce' (c : _ -> Comp _) (v : Vector.t _ numBytes), refine (c (addE ce 8)) (ret (build_aligned_ByteString v, ce')) -> refine (((format_word (monoidUnit := ByteString_QueueMonoidOpt) w) ThenC c) ce) (ret (build_aligned_ByteString (Vector.cons _ w _ v), ce')).
proof: Proof. unfold compose; intros. unfold Bind2. setoid_rewrite aligned_format_char_eq; simplify with monad laws. simpl; rewrite H; simplify with monad laws. simpl. rewrite <- build_aligned_ByteString_append. 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