proposition: Lemma format_list_as_foldl encode_A : forall xs env, encode_list encode_A xs env = fold_left (format_list_body encode_A) xs (mempty, env).
proof: Proof. induction xs; simpl. + reflexivity. + intros; destruct (encode_A _ _). rewrite IHxs, mempty_left, (format_list_body_characterization encode_A xs t c). destruct (fold_left _ _ _); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.Base.FixFormat Coq.Lists.List