proposition: Lemma refine_addCacheToADT Sig oldConstrs oldMeths : refineADT (@Build_ADT Sig rep oldConstrs oldMeths) (@Build_ADT Sig cachedRep (fun idx => addCacheToConstructor (oldConstrs idx)) (fun idx => addCacheToMethod (oldMeths idx))).
proof: Proof. eapply refineADT_Build_ADT_Rep; eauto using refine_addCacheToConstructor, refine_addCacheToMethod. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv