proposition: Lemma refine_addCacheToMethod_step {Dom : list Type} {Cod : option Type} (oldMethod : methodType rep Dom Cod) (newMethod : methodType cachedRep Dom Cod) : @refineMethod_eq cachedRep _ _ (addCacheToMethod oldMethod) newMethod -> @refineMethod rep cachedRep cachedRep_AbsR _ _ oldMethod newMethod.
proof: Proof. intros; eapply refineMethod_eq_trans; eauto using refine_addCacheToMethod. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT Coq.Sets.Ensembles Fiat.ADTRefinement Fiat.ADTRefinement.Refinements.ADTRepInv