Allow onSuccess to fail. This is necessary to prevent soundness issues.

The synthesizer used to generate wrong programs by generating inductive
programs with an impossible base-case. onSuccess on inductive rules now
prevents this by checking that sufficiently many cases have precondition
== true. Otherwise, onSuccess fails. This last-moment failure is now
handled correctly.

Strenghten precondition