setup for refined facts handling; tuned insert_facts, assumption, (un)fold; insert_tac: no rotate_tac, order was OK in the first place; added ctxt_args, bang_sectioned_args; added assm_tac;