proposition: Lemma IList_encode'_body_simpl : forall (cache : Cache.Cache) {av HD bin : Type} (transformer : Transformer.Transformer bin) f acc (head: HD) (tail: _ -> Telescope av) ext, TelEq ext ([[ ret (IList.IList_encode'_body cache transformer f acc head) as v ]] :: tail v) ([[ ret (f head (snd acc)) as v ]] :: tail (Transformer.transform (fst acc) (fst v), (snd v))).
proof: Proof. intros; unfold IList.IList_encode'_body; destruct acc. rewrite TelEq_let_ret2; reflexivity. Qed.
imports: CertifiedExtraction.Core CertifiedExtraction.TelAppend CertifiedExtraction.ExtendedLemmas CertifiedExtraction.ExtendedPropertiesOfTelescopes CertifiedExtraction.Extraction.BinEncoders.Basics