Theorem Equiv.Perm.mul_apply

Modification history