Theorem Equiv.Perm.one_apply

Modification history