proposition: Lemma format_words {n m} (addE_addE_plus : forall ce n m, addE (addE ce n) m = addE ce (n + m)) : forall (w : word (n + m)) ce, refine (format_word (monoidUnit := ByteString_QueueMonoidOpt) w ce) ((format_word (monoidUnit := ByteString_QueueMonoidOpt) (split2 m n (eq_rect _ _ w _ (trans_plus_comm _ _))) ThenC (format_word (monoidUnit := ByteString_QueueMonoidOpt) (split1 m n (eq_rect _ _ w _ (trans_plus_comm _ _))))) ce).
proof: Proof. intros; rewrite format_words'. rewrite split1'_eq, split2'_eq; reflexivity. eauto. 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