Allow IH calls in `suffices by`

[tsani]

We currently forbid IH appeals in suffices by because the interaction with the totality checker is not obvious. It's complicated enough to get termination checking to work in ordinary by, but with suffices by it is even more complicated because the term is not yet constructed.

For example, suppose f : A -> B is proven by induction on the argument a : A. Suppose further you're in a subgoal of type B, and you want to use suffices by f toshow A to solve the subgoal. How can we then in the subgoal for A be sure that the constructed term is a subterm of a? I haven't thought too hard about it, so perhaps the answer is obvious, but it isn't jumping out at me.

[tsani]

I'm removing this from milestone 1 because it's tricky to implement and not essential for our paper.