This PR aims to add lambda support. To that end, the following changes have been made:

• A new typeclass LawfulHeap has been added. This denotes the types that can be argued with separation logic predicates. Implementors must define the operations (union and disjoint) and prove some fundamental theorems about them. SLP now works over all types that implement LawfulHeap. State _ has been replaced with two types that implement LawfulHeap: ValHeap and State where ValHeap is the old state and State is a wrapper around ValHeap that adds a set of lambdas. We can construct lambda singletons with the [r ↣ l] which means r refers to the lambda l. This is a big change, and required many changes across the codebase.
• AST: A new structure Lambda is introduced. A lambda expression Expr.lam is introduced. Moreover, FunctionIdent is extended to support references to lambda functions in the environment. Accordingly, lambda calls can be represented with Expr.calls.
• Syntax: New syntax for creating and calling lambdas have been introduced. Lambdas can be constructed as
  let add = |a, b| : u8, u8 -> u8 { ... }, and they can be called with ^add(4 : u8, 7 : u8)
• Semantics: Two new Omni rules (one for creating a lambda and one for calling lambdas) were added. A new theorem nested_triple is added that can be used by the steps tactic to deconstruct the goals of form P {e} Q with introduction rules of form {P1} e1 {Q} -> {P1 * H} e2 {Q * H}, like callLambda_intro. Corresponding introduction rules were added and integrated into the steps tactic.

Closes #6