[CN] Use a auto-unfolding scheme for functions

[dc-mak]

We currently have an auto-unfolding scheme for predicates that works quite well in practice, yet for functions we have an one which requires manual unfolding at each step.

In cases like doubly-linked queue lemmas, the unfolding gets rather tedious to specify, since the SMT solver already has all the available information to know which branch to select.

In the absence of #260, this gets even more annoying when there are instances where to even specify the arguments of what to unfold, you need to do a take beforehand (see queue_pop_unified.c from the tutorial - the lemmas are ultimately just unfoldings).

This would also bring us closer to unification of the two languages (at least in the internal representation if not in the user facing syntax) #304.