===== subgoal_tac =====
Adds a formula to the assumptions but adds a subgoal to prove it from the current ones.