An exact proof term for the current goal is R_standard_basis_is_basis_local.