test(tests/lean): add nested 'have' expression test

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

tests/lean/nested_have.lean

@@ -0,0 +1,15 @@
+import macros
+
+theorem T (a b c d e : Bool) : (a → b) → (a → b → c) → d ∧ a → (d → c → e) → e
+:= assume Hab Habc Hda Hde,
+     have Hd : d,
+       from and_eliml Hda,
+     have Ha : a,
+       from and_elimr Hda,
+     have Hc : c,
+       from (have Hb : b,
+               from Hab Ha,
+             show c,
+               from Habc Ha Hb),
+     show e,
+       from Hde Hd Hc

tests/lean/nested_have.lean.expected.out

@@ -0,0 +1,4 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Imported 'macros'
+  Proved: T