proposition: Lemma domcod_old_to_new_resp_inf_1' {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall P, refineFun (@domcod_old_to_new _ _ fDom fCod AbsR (cl_inf P)) (cl_inf (fun f => exists f', P f' /\ refineFun (@domcod_old_to_new _ _ fDom fCod AbsR f') f)).
proof: Proof. intros; eapply (glb_refineFun_inf _ (fun f => exists f', P f' /\ refineFun (@domcod_old_to_new _ _ fDom fCod AbsR f') f)). simpl; intros; destruct_ex; intuition subst. rewrite <- H1. eapply domcod_old_to_new_monotone. eapply (glb_refineFun_inf _ 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