proposition: Lemma refineFun_To_refineFunAbsR {oldRep newRep} (AbsR : oldRep -> newRep -> Prop) {fDom : list Type} {fCod : Type} : forall (fDef : funType (oldRep :: fDom) (oldRep * fCod)) (fDef' : funType (newRep :: fDom) (newRep * fCod)), refineFun (domcod_old_to_new AbsR fDef) fDef' <-> refineFun_AbsR AbsR fDef fDef'.
proof: Proof. simpl. unfold refineFun_AbsR, domcod_old_to_new; split. - induction fDom; simpl; intros; eauto. + unfold refine; intros. eapply H in H1; computes_to_inv; subst; eauto. + intros; eapply (IHfDom (fun r => fDef r t) (fun r => fDef' r t)); eauto. intros; eapply H. - induction fDom; simpl; intros; eauto. + unfold refine; intros. computes_to_econstructor; intros. eapply H in H0; computes_to_inv; subst; eauto. + intros; eapply (IHfDom (fun r => fDef r t0) (fun r => fDef' r t0)); 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