is mentioned by

Thm* (P P) False

[prop_iff_contra]

In prior sections: core