fix(kernel/converter): missing case: two constants c.{l1} and c.{l2} where l1 and l2 are structurally different but equivalent (or can be made equivalent)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): when imitating (f a), abstract local constants occurring in f

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(lean/run): add elaborator tests

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(tests/lua/tc_bug1): update test to reflect recent changes

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>