diff --git a/tests/lean/run/eq12.lean b/tests/lean/run/eq12.lean
new file mode 100644
index 0000000000..6fa6fb099d
--- /dev/null
+++ b/tests/lean/run/eq12.lean
@@ -0,0 +1,22 @@
+open nat bool inhabited
+
+definition diag : bool → bool → bool → nat,
+diag _  tt ff := 1,
+diag ff _  tt := 2,
+diag tt ff _  := 3,
+diag _  _  _  := default nat
+
+theorem diag1 (a : bool) : diag a tt ff = 1 :=
+bool.cases_on a rfl rfl
+
+theorem diag2 (a : bool) : diag ff a tt = 2 :=
+bool.cases_on a rfl rfl
+
+theorem diag3 (a : bool) : diag tt ff a = 3 :=
+bool.cases_on a rfl rfl
+
+theorem diag4_1 : diag ff ff ff = default nat :=
+rfl
+
+theorem diag4_2 : diag tt tt tt = default nat :=
+rfl
diff --git a/tests/lean/run/eq13.lean b/tests/lean/run/eq13.lean
new file mode 100644
index 0000000000..b21753200d
--- /dev/null
+++ b/tests/lean/run/eq13.lean
@@ -0,0 +1,16 @@
+open nat inhabited
+
+definition f : nat → nat → nat,
+f _ 0 := 0,
+f 0 _ := 1,
+f _ _ := 2
+
+theorem f_zero_right : ∀ a, f a 0 = 0,
+f_zero_right 0        := rfl,
+f_zero_right (succ _) := rfl
+
+theorem f_zero_succ (a : nat) : f 0 (a+1) = 1 :=
+rfl
+
+theorem f_succ_succ (a b : nat) : f (a+1) (b+1) = 2 :=
+rfl