Thm* eq_int_eq_false_elim

Thm* eq_int_eq_false

Thm* eqff_to_assert

Thm* not_assert_elim

Thm* assert_of_ff

Thm* band_ff_simp

Thm* bor_ff_simp

Thm* bool_ind

Thm* bool_cases

Thm* btrue_neq_bfalse