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