ANTS_TAC : tactic
Split off antecedent of antecedent of goal as a new subgoal.
A ?- (p ==> q) ==> r ======================= ANTS_TAC A ?- p A ?- q ==> r
Fails unless the goal is of the specified form.
Convenient for focusing on assumptions of an implicational theorem that one wants to use.