fact: Fixpoint refineFun_AbsR' {oldRep newRep} (fDom : list Type) (fCod : Type) (AbsR : oldRep -> newRep -> Prop) (fDef : funType fDom (oldRep * fCod)) (fDef' : funType fDom (newRep * fCod)) {struct fDom} : Prop := match fDom as fDom' return funType fDom' (oldRep * fCod) -> funType fDom' (newRep * fCod) -> Prop with | List.nil => fun fDef fDef' => refine (cod_old_to_new AbsR fDef) fDef' | List.cons T fDom' => fun fDef fDef' => forall (t : T), refineFun_AbsR' fDom' fCod AbsR (fDef t) (fDef' t) end fDef fDef'.
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