proposition: Lemma refineConstructor_trans rep rep' rep'' Dom AbsR AbsR' : forall c c' c'', @refineConstructor rep rep' AbsR Dom c c' -> @refineConstructor rep' rep'' AbsR' Dom c' c'' -> refineConstructor (fun r_o r_n => exists r_o', AbsR r_o r_o' /\ AbsR' r_o' r_n) c c''.
proof: Proof. induction Dom. - intro; simpl; intros; subst; intros v Comp_v. apply H0 in Comp_v; computes_to_inv; subst. apply H in Comp_v; computes_to_inv; subst; eauto. - simpl; intros; eapply IHDom; simpl in *. apply H. eapply H0. Qed.
imports: Fiat.Common Fiat.Computation Coq.Sets.Ensembles Fiat.ADT.ADTSig Fiat.ADT.Core Fiat.ADTRefinement.Core