proposition: Lemma refine_absMethod (dom : list Type) (cod : option Type) (oldMethod : methodType oldRep dom cod) : @refineMethod oldRep newRep AbsR _ _ oldMethod (absMethod oldMethod).
proof: Proof. induction dom. - simpl in *; unfold refineMethod, refineMethod', absMethod, absMethod', refine; intros; destruct cod; intros; computes_to_inv. + destruct (H0 _ H) as [or' [Comp_or [AbsR_or'' eq_or''] ] ]. repeat computes_to_econstructor; eauto. destruct v; simpl in *; subst; econstructor. + destruct (H0 _ H) as [or' [Comp_or AbsR_or'' ] ]. repeat computes_to_econstructor; eauto. - intro; simpl; intros. eapply (IHdom (fun or => oldMethod or d)); eauto. Qed.
imports: Fiat.Common Fiat.Computation Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core Fiat.ADTRefinement.SetoidMorphisms Fiat.ADTRefinement.GeneralRefinements