An exact proof term for the current goal is (lemma_topology_from_basis R R_standard_basis R_standard_basis_is_basis_local).