Theorem Equiv.arrowCongr_trans

Modification history