fact: Record family : Type := mkfamily {ind : R -> Prop; f :> R -> R -> Prop; cond_fam : forall x:R, (exists y : R, f x y) -> ind x}.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type