ifThen1ToSolution

->/2 request goals over ifThenTheory1 and their expected Solutions, checking that the then (->/2) combinator commits to the first solution of its condition (here, a(1)) and never backtracks into it.