Given a goal of the form A ?- ((p ==> q) ==> r), an application of
impl_tac will produce two sub-goals: A ?- p and A, p ?- (q ==> r).
This can be useful if p should be dealt with in isolation, when,
say, the tactics that solve p can’t safely be applied to q and/or
This tactic differs from impl_tac in that it keeps p as an
assumption in the second sub-goal.