THM	assert_iff_btrue	P:. P P = tt
THM	assert_iff_btrue_rw	P:. {P P = tt}
THM	not_assert_iff_bfalse	P:. P P = ff
ML	ab_assert	add_AbReduce_conv `assert_eval` assert_evalC;;
THM	assert_of_bool_eq_bfalse_false	b:. b b =b ff = ff
THM	assert_of_eq_bool_iff_equal_bool	b1,b2:. b1 =b b2 b1 = b2

the other theories