Theorem neg_apply

Modification history