prevent unnecessary fixpoints in elaboration

[pigumar1]

This PR tries to fix #1268 by checking if there are self-references in the function body/bodies during elaboration and decide whether to include the fixpoint based on that information.

For potential mutual recursive functions, the fixpoint is included as long as one of the function names occur in the definition as a free variable (by looking at the co-context)

A non-recursive function:

A recursive function:

Non-recursive functions:

Mutual recursive functions: