I am using the SDHC card on HPS Linux.
The theoretical value of operation clock is 50 MHz.
I think that it is set to 50 MHz and it is displayed also in the Linux start log as follows.
mmc_host mmc 0: Bus speed (slot 0) = 200000000 Hz (slot req 50000000 Hz, actual 50000000 HZ div = 2)
However, if you actually put the SDHC card in and operate it, it is operating at 12.5 MHz.
I confirmed it with an oscilloscope.