proposition: Lemma encode_list_post_transform_TelEq : 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 (tenv: _ -> Telescope av) ext (g: B -> B'), 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 ([[ret (fold_on Transformer.transform_id) as folded]] ::[[ k__stream ->> g (Transformer.transform base (fst folded)) as _]] :: tenv folded) ([[ret (fold_on base) as folded]] ::[[ k__stream ->> g (fst folded) as _]] :: tenv folded).
proof: Proof. cbv zeta; intros * H. setoid_rewrite Propagate_anonymous_ret. rewrite (encode_list_body_characterization _ _ base). destruct (List.fold_left _ _ _); simpl; erewrite H; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.TelAppend CertifiedExtraction.ExtendedLemmas CertifiedExtraction.ExtendedPropertiesOfTelescopes CertifiedExtraction.Extraction.BinEncoders.Basics