Theorem Equiv.prodCongr_refl_right

Modification history