proposition: Lemma cod_old_to_new_monotone {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall (fDef fDef' : funType fDom (oldRep * fCod)), refineFun fDef fDef' -> refineFun (cod_old_to_new AbsR fDef) (cod_old_to_new AbsR fDef').
proof: Proof. induction fDom; simpl; intros. - setoid_rewrite H; reflexivity. - simpl; 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