proposition: Lemma refineFunAbsR_domcod_old_to_new {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall (fDef : funType (oldRep :: fDom) (oldRep * fCod)), refineFun_AbsR AbsR fDef (domcod_old_to_new AbsR fDef).
proof: Proof. intros. unfold refineFun_AbsR, domcod_old_to_new. under_fDom. { unfold refine; intros. computes_to_inv; destruct_ex; intuition eauto; subst. } 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