Thm* ite_rw_true

Thm* ite_rw_false

Thm* assert_of_le_int

Thm* assert_of_bimplies

Thm* assert_of_bor

Thm* assert_of_band

Thm* assert_of_bnot

Thm* assert_of_eq_bool

Thm* assert_of_eq_int_rw

Thm* assert_of_lt_int

Thm* neg_assert_of_eq_atom

Thm* neg_assert_of_eq_int

Thm* assert_of_eq_int

Thm* assert_of_eq_atom

Thm* iff_imp_equal_bool

Thm* decidable__assert

Thm* eqff_to_assert

Thm* eqtt_to_assert

Thm* not_assert_elim

Thm* assert_elim

Thm* assert_of_ff

Thm* assert_of_tt

Thm* assert_functionality_wrt_bimplies

Thm* bimplies_transitivity

Thm* bimplies_weakening

Thm* comb_for_assert_wf