split bool_ctxt up and move it out into separate theories

also, make it generic, i.e. mk_bool_ctxt ctxt adds the boolean
definitions to an arbitrary initial ctxt. more general for proving
theorems about. similarly mk_eta_ctxt, mk_select_ctxt, ...