b1,b2:
. b1=
b2 
b1 = b2b:. b b=false = falseP:. 
P P = falseP:. P P = trueP:. P P = true
b == if b
True else False fi
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] |
| Thm* P:. P P = false | [not_assert_iff_bfalse] |
| Thm* P:. P P = true | [assert_iff_btrue_rw] |
| Thm* P:. P P = true | [assert_iff_btrue] |
In prior sections: bool 1