SUFF_TAC
Tactic.SUFF_TAC : term -> tactic
Introduces an implicational subgoal.
A call to SUFF_TAC t on the goal asl ?- g introduces two subgoals:
asl ?- t ==> g and asl ?- t. At a high-level, the user's claim is
that term t suffices (hence the name) to prove the goal. The first new
goal to be discharged is the check for this; the second is to actually
show t.
Failure
Will fail if t is not of type :bool.