proposition: Lemma IList_encode'_body_as_compose {HD bin : Type} : forall (cache : Cache.Cache) (transformer : Transformer.Transformer bin) f acc (head: HD), (IList.IList_encode'_body cache transformer f acc head) = Compose.compose transformer (fun c => (fst acc, c)) (f head) (snd acc).
proof: Proof. intros; unfold IList.IList_encode'_body, Compose.compose; simpl. destruct acc; simpl; destruct (f _ _); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega