bool
1
Doc
Def
b2i(b) == if b
1 else 0 fi
Thm*
b2i_bounds
Thm*
comb_for_b2i_wf