proposition: Lemma refineMethod_trans rep rep' rep'' Dom Cod AbsR AbsR' : forall m m' m'', @refineMethod rep rep' AbsR Dom Cod m m' -> @refineMethod rep' rep'' AbsR' Dom Cod m' m'' -> refineMethod (fun r_o r_n => exists r_o', AbsR r_o r_o' /\ AbsR' r_o' r_n) 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. repeat computes_to_econstructor; 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. eapply (IHDom (fun d' => m r_o d) (fun d' => m' x d) (fun d' => m'' r_n d)); eauto. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core