Thm* assert_of_bnot

Thm* eqff_to_assert

Thm* bnot_of_le_int

Thm* bnot_thru_bor

Thm* bnot_thru_band

Thm* bnot_bnot_elim

Thm* comb_for_bnot_wf