An exact proof term for the current goal is (lemma_topology_from_basis R (R_standard_basis ∪ R_K_basis) R_standard_plus_K_basis_is_basis_local).