Apply a theorem-tactic using a proposition that can be assumed without loss of
generality.
DESCRIPTION
Like wlog_tac, but the theorem P |- P is passed to the user-provided
theorem-tactic instead of strip_assume_tac.
FAILURE
Never fails when applied to a theorem-tactical. The resulting tactic fails if
and only if the user-provided theorem-tactical fails when used as a tactic
(i.e.: when applied to a theorem and a goal).