fact: Definition corec_rec_family I A B (M:family I B) (P:A->Prop) (R:binary A) : family (I*A) (A->B) := let R' := lexico2 (family_r M) (tclosure R) in Build_family R' (fun p f1 f2 => let (i,x) := p : I*A in forall i' x', rclosure R' (i',x') (i,x) -> P x' -> family_sim M i' (f1 x') (f2 x')).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)