proposition: Lemma FixList_is_IList : forall (A bin : Type) (cache : Cache.Cache) (transformer : Transformer.Transformer bin) (A_encode : A -> Cache.CacheEncode -> bin * Cache.CacheEncode) (xs : list A) (env : Cache.CacheEncode), @FixList.FixList_encode' A bin cache transformer A_encode xs env = @IList.IList_encode' A bin cache transformer A_encode xs env.
proof: Proof. induction xs; simpl; intros. + reflexivity. + destruct (A_encode _ _). rewrite IHxs; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega