proposition: Lemma encode_list_post_transform_TelEq_TelAppend : forall {av} {A B B': Type} (cache : Cache.Cache) (transformer : Transformer.Transformer B) (A_encode : A -> Cache.CacheEncode -> B * Cache.CacheEncode) (xs : list A) (base : B) (env : Cache.CacheEncode) k__stream ext (tenv: _ -> Telescope av) (g: B -> B') tenv', let fold_on b := List.fold_left (encode_list_body A_encode) xs (b, env) in (forall a1 a2 b, tenv (a1, b) = tenv (a2, b)) -> TelEq ext (TelAppend ([[ret (fold_on Transformer.transform_id) as folded]] ::[[ k__stream ->> g (Transformer.transform base (fst folded)) as _]] :: tenv folded) tenv') (TelAppend ([[ret (fold_on base) as folded]] ::[[ k__stream ->> g (fst folded) as _]] :: tenv folded) tenv').
proof: Proof. simpl; intros. apply encode_list_post_transform_TelEq; intros; erewrite H; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.TelAppend CertifiedExtraction.ExtendedLemmas CertifiedExtraction.ExtendedPropertiesOfTelescopes CertifiedExtraction.Extraction.BinEncoders.Basics