proposition: Lemma refine_addCacheTo_BuildADT (n m : nat) (consSigs : Vector.t consSig n) (methSigs : Vector.t methSig m) (consDefs : ilist (B := @consDef rep) consSigs) (methDefs : ilist (B := @methDef rep) methSigs) : refineADT (BuildADT consDefs methDefs) (BuildADT (imap addCacheToConsDef consDefs) (imap addCacheToMethDef methDefs)).
proof: Proof. generalize (refine_addCacheToADT cacheSpec (BuildADTSig consSigs methSigs) (fun idx => getConsDef consDefs idx) (fun idx => getMethDef methDefs idx)); eauto; intros. econstructor; intros. - simpl Constructors; rewrite <- ith_imap. apply refine_addCacheToConstructor. - simpl Methods; rewrite <- ith_imap. apply refine_addCacheToMethod. Qed.
imports: Coq.Lists.List Fiat.Common Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTNotation.BuildADTSig Fiat.ADTNotation.BuildADT Fiat.Common.ilist Fiat.Common.BoundedLookup Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements Fiat.ADTRefinement.Refinements.HoneRepresentation Fiat.ADTRefinement.BuildADTSetoidMorphisms Fiat.ADTRefinement.Refinements.ADTCache