got rid of (old) antiframe in the prover

also some code cleanup
a few comments

(about how I'll change [apply_rule_list] to handle abduction)