is mentioned by

Thm* b1,b2:. b1=b2 b1 = b2	[assert_of_eq_bool_iff_equal_bool]
Thm* b:. b b=false = false	[assert_of_bool_eq_bfalse_false]

In prior sections: bool 1