From b60c9d9ecc911905dfca7bb9acaf198af06a6e9e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Aug 2014 21:23:14 -0700
Subject: [PATCH] test(tests/lean/run): add test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 tests/lean/run/over_subst.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 tests/lean/run/over_subst.lean

diff --git a/tests/lean/run/over_subst.lean b/tests/lean/run/over_subst.lean
new file mode 100644
index 000000000..b53601068
--- /dev/null
+++ b/tests/lean/run/over_subst.lean
@@ -0,0 +1,33 @@
+import logic
+
+namespace nat
+variable nat : Type.{1}
+variable add : nat → nat → nat
+variable le : nat → nat → Prop
+variable one : nat
+infixl `+`:65 := add
+infix `≤`:50 := le
+axiom add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
+axiom add_le_left {a b : nat} (H : a ≤ b) (c : nat) : c + a ≤ c + b
+end nat
+
+namespace int
+variable int : Type.{1}
+variable add : int → int → int
+variable le : int → int → Prop
+variable one : int
+infixl `+`:65 := add
+infix `≤`:50  := le
+axiom add_assoc (a b c : int) : (a + b) + c = a + (b + c)
+axiom add_le_left {a b : int} (H : a ≤ b) (c : int) : c + a ≤ c + b
+abbreviation lt (a b : int) := a + one ≤ b
+infix `<`:50  := lt
+end int
+
+using int
+using nat
+
+set_option unifier.expensive true
+
+theorem add_lt_left {a b : int} (H : a < b) (c : int) : c + a < c + b :=
+subst (symm (add_assoc c a one)) (add_le_left H c)