Write unit tests for elabApply and unApply

[facundominguez]

These functions are used to encode and decode higher-order functions into a form where all function arguments are replaced with integers.

They are in Language.Fixpoint.SortCheck.

This transformation is necessary because the SMT solver doesn't support higher-order functions.

The code could use some documentation explaining when does the function insert apply calls and when not. This is likely to be discovered as part of writing some tests and reading the code.