is mentioned by

Thm* b:. b b=false = false	[assert_of_bool_eq_bfalse_false]
Thm* P:. P P = false	[not_assert_iff_bfalse]

In prior sections: bool 1