fact: Fixpoint encode_list (encode_A : A -> CacheFormat -> T * CacheFormat) (xs : list A) (ce : CacheFormat) : T * CacheFormat := match xs with | nil => (mempty, ce) | x :: xs' => let (b1, env1) := encode_A x ce in let (b2, env2) := encode_list encode_A xs' env1 in (mappend b1 b2, env2) end%comp.
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