proposition: Lemma refineFun_AbsR'_trans {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall (fDef fDef'' : funType fDom (oldRep * fCod)) (fDef' : funType fDom (newRep * fCod)), refineFun fDef fDef'' -> refineFun_AbsR' _ _ AbsR fDef'' fDef' -> refineFun_AbsR' _ _ AbsR fDef fDef'.
proof: Proof. intros. induction fDom; simpl in *; intros; eauto. rewrite <- H0; eauto. unfold refine; intros; computes_to_inv; destruct_ex; intuition 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