Theorem supSupₛHom_apply

Modification history