Theorem Equiv.trans_cancel_right

Modification history