Thm* eq_int_eq_true_elim

Thm* eq_int_eq_false_elim

Thm* eq_int_eq_true

Thm* eq_int_eq_false

Thm* fun_thru_ite

Thm* ite_rw_true

Thm* ite_rw_false

Thm* assert_of_bimplies

Thm* assert_of_bor

Thm* assert_of_band

Thm* assert_of_bnot

Thm* assert_of_eq_bool

Thm* iff_imp_equal_bool

Thm* decidable__assert

Thm* eqff_to_assert

Thm* eqtt_to_assert

Thm* not_assert_elim

Thm* assert_elim

Thm* band_tt_simp

Thm* band_ff_simp

Thm* bor_tt_simp

Thm* bor_ff_simp

Thm* assert_functionality_wrt_bimplies

Thm* bimplies_transitivity

Thm* bimplies_weakening

Thm* bnot_of_le_int

Thm* bnot_thru_bor

Thm* bnot_thru_band

Thm* bnot_bnot_elim

Thm* decidable__equal_bool

Thm* bool_ind

Thm* bool_cases

Thm* btrue_neq_bfalse

Thm* comb_for_bimplies_wf

Thm* comb_for_bor_wf

Thm* comb_for_band_wf

Thm* comb_for_bnot_wf

Thm* b2i_bounds

Thm* comb_for_b2i_wf

Thm* comb_for_assert_wf

Thm* ifthenelse_wf