Introduces terminates(f(..)) witnesses in the spec, used to generate
safe recursive calls.

After a split i.e. on a List with Cons, the witness becomes

terminates(f(.., Cons(h, t), ..))

at which point we know that calling f(.., t, ..) is safe
termination-wise.