Theorem Equiv.Perm.subtypeCongr.left_apply

Modification history