fact: Definition FinEnum_ball (e:Q) (x y:list X) := hausdorffBall X e (fun a => InFinEnumC a x) (fun a => InFinEnumC a y).
imports: CoRN.model.totalorder.QposMinMax CoRN.metric2.Hausdorff CoRN.logic.Classic CoRN.stdlib_omissions.List CoRN.metric2.Classification CoRN.metric2.Complete CoRN.metric2.Prelength