proposition: Lemma domcod_old_to_new_resp_sup_2' {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall P, P (refineFun_sup P) -> refineFun (@domcod_old_to_new _ _ fDom fCod AbsR (cl_sup P)) (cl_sup (fun f => exists f', P f' /\ refineFun f (@domcod_old_to_new _ _ fDom fCod AbsR f'))).
proof: Proof. intros. eapply (lub_refineFun_sup _ (fun f => exists f', P f' /\ refineFun f (@domcod_old_to_new _ _ fDom fCod AbsR f'))). eexists (refineFun_sup P); intuition. 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