An exact proof term for the current goal is (lemma_topology_from_basis X (famunion X (λx ⇒ {open_ball X d x r|r ∈ R, Rlt 0 r})) (open_balls_form_basis X d Hd)).