proposition: Lemma refine_addCacheToMethod {Dom : list Type} {Cod : option Type} (oldMethod : methodType rep Dom Cod) : @refineMethod rep cachedRep cachedRep_AbsR _ _ oldMethod (addCacheToMethod oldMethod).
proof: Proof. unfold refineMethod, addCacheToMethod, methodType, cachedRep_AbsR, refine in *; intros; intuition; subst. induction Dom; simpl. - destruct Cod. + unfold cachedRep_AbsR in *; intuition; subst. repeat (f_equiv; intro). computes_to_inv; subst. repeat computes_to_econstructor. simpl; split; eauto. + unfold cachedRep_AbsR in *; intuition; subst. repeat (f_equiv; intro). computes_to_inv; subst. repeat computes_to_econstructor. simpl; split; eauto. - intros; eapply (IHDom (fun r_n => oldMethod r_n d)). Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv