proposition: Lemma refine_sequence_Format {cache : Cache} {S T : Type} {monoid : Monoid T} (format1 format2 : FormatM S T) : forall s env, refineEquiv ((format1 ++ format2) s env) ((fun (s : S) => (ComposeOpt.compose _ (format1 s) (format2 s))) s env).
proof: Proof. reflexivity. Qed.
imports: Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Computation.Refinements.General Fiat.Narcissus.BaseFormats