Theorem Equiv.Perm.subtypeCongr.right_apply

Modification history