proposition: Lemma domcod_old_to_new_resp_sup_1' {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall P, refineFun (cl_sup (fun f => exists f', P f' /\ refineFun f (@domcod_old_to_new _ _ fDom fCod AbsR f'))) (@domcod_old_to_new _ _ fDom fCod AbsR (cl_sup P)) .
proof: Proof. intros; eapply (lub_refineFun_sup _ (fun f => exists f', P f' /\ refineFun f (@domcod_old_to_new _ _ fDom fCod AbsR f'))). simpl; intros; destruct_ex; intuition subst. rewrite H1. eapply domcod_old_to_new_monotone. eapply (lub_refineFun_sup _ P); eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT Fiat.ADTNotation Fiat.Computation.FixComp Coq.ZArith.ZArith Coq.Arith.PeanoNat Fiat.Common.Frame Fiat.ADTRefinement Fiat.ADTRefinement.BuildADTRefinements