feat(library/simplifier): support for dependent simplification in lambda expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/parser): allow the user to write (Type) without providing a level

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(frontends/lean/frontend): the definition of the explicit version @f must be definitionally equal to f

Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/simplifier): support for dependent simplification in Pi/forall expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/simplifier): fix style

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(library/simplifier): fix style