is mentioned by

Thm* P:. P P = true

[assert_iff_btrue_rw]

In prior sections: core well fnd int 1 bool 1