test(frontends/lean): add example showing higher order matching is working, and is useful

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

tests/lean/ho.lean

@@ -0,0 +1,7 @@
+Variable g {A : Type} (a : A) : A
+Variable a : Int
+Variable b : Int
+Axiom H1 : a = b
+Axiom H2 : (g a) > 0
+Theorem T1 : (g b) > 0 := Subst _ H2 H1
+Show Environment 2

tests/lean/ho.lean.expected.out

@@ -0,0 +1,10 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: g
+  Assumed: a
+  Assumed: b
+  Assumed: H1
+  Assumed: H2
+  Proved: T1
+Axiom H2 : (g a) > 0
+Theorem T1 : (g b) > 0 := Subst (λ x : ℤ, if Bool ((g x) ≤ 0) ⊥ ⊤) H2 H1