proposition: Lemma refineFun_AbsR_trans' {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall (fDef : funType (oldRep :: fDom) (oldRep * fCod)) (fDef' fDef'' : funType (newRep :: fDom) (newRep * fCod)), refineFun fDef'' fDef' -> refineFun_AbsR AbsR fDef fDef'' -> refineFun_AbsR AbsR fDef fDef'.
proof: Proof. intros. unfold refineFun_AbsR in *. induction fDom; simpl in *; intros. rewrite (H0 _ _ H1). exact (H _). apply (IHfDom (fun r => fDef r t) (fun r => fDef' r t) (fun r => fDef'' r t)); 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