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.