Sound equality checking for Lambda

[joscoh]

Issue #, if available:

Description of changes: Previously, Lambda's equality checking was unsound (when compared against an in-progress denotational semantics). This was partially fixed in #633, but it involved an awkward mechanism that prevented equality checking under lambdas. It was also still unsound, since we cannot erase types when comparing equality (e.g. @Nil int is not semantically equal to @Nil bool).

This PR adds a more principled equality check that is sound but incomplete, giving up if it cannot prove equality of inequality. It tries syntactic equality (which can prove equality, not inequality), reasons about constants, proves equality and inequality of lambdas extensionally, and reasons about the (in)equality of datatype constructors by using injectivity+disjointness properties. Tests demonstrating its behavior are in LExprEqTests.lean.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[andrewmwells-amazon]

Code LGTM. Left a suggestion for an outdated comment.

[aqjune-aws]

During a separate discussion on the slack channel, I became to have a curiosity - does this fast-forwarded path actually still allow Nil without any type annotation to still compare equal? If the two Nils are annotated with different types, does it imply that type annotation may change evaluation result?

[joscoh]

Yes, two Nil without type annotations are considered equal and yes, if they are annotated with different types, the evaluation result may change. I think this is fine. Our semantics are defined only after type inference, when the annotation is uniquely determined. Essentially, we make no guarantees about the behavior of the evaluator (except that it is consistent with Step) on untyped terms.