proposition: Lemma refineMethod_eq_trans rep rep' Dom Cod AbsR : forall m m' m'', @refineMethod rep rep' AbsR Dom Cod m m' -> @refineMethod_eq rep' Dom Cod m' m'' -> refineMethod AbsR m m''.
proof: Proof. unfold refineMethod, methodType; induction Dom. - intro; simpl; intros; destruct Cod; subst; intros v Comp_v. + destruct_ex; intuition. eapply H0 in Comp_v; eauto; computes_to_inv; subst. eapply H in Comp_v; eauto; computes_to_inv; subst; eauto. + destruct_ex; intuition. eapply H0 in Comp_v; eauto; computes_to_inv; subst. eapply H in Comp_v; eauto; computes_to_inv; subst; eauto. - simpl; intros. destruct_ex; intuition. unfold refineMethod_eq in *. eapply (IHDom (fun r_o => m r_o d) (fun r_n => m' r_n d) (fun r_n => m'' r_n d)); eauto. intros; eapply H0. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core