diff --git a/tests/lean/run/cody1.lean b/tests/lean/run/cody1.lean
new file mode 100644
index 000000000..9db70c9f2
--- /dev/null
+++ b/tests/lean/run/cody1.lean
@@ -0,0 +1,24 @@
+import logic
+
+abbreviation subsets (P : Type) := P → Prop.
+
+section
+
+hypothesis A : Type.
+
+hypothesis r : A → subsets A.
+
+hypothesis i : subsets A → A.
+
+hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
+
+definition delta (a:A) : Prop := ¬ (r a a).
+
+notation `δ` := delta.
+
+-- Crashes unifier!
+theorem false_aux : ¬ (δ (i delta))
+         := assume H : δ (i delta),
+            have H' : r (i delta) (i delta),
+              from eq_rec H (symm retract),
+            H H'.
diff --git a/tests/lean/run/cody2.lean b/tests/lean/run/cody2.lean
new file mode 100644
index 000000000..ac356b33d
--- /dev/null
+++ b/tests/lean/run/cody2.lean
@@ -0,0 +1,23 @@
+import logic
+
+abbreviation subsets (P : Type) := P → Prop.
+
+section
+
+hypothesis A : Type.
+
+hypothesis r : A → subsets A.
+
+hypothesis i : subsets A → A.
+
+hypothesis retract {P : subsets A} {a : A} : r (i P) a = P a.
+
+definition delta (a:A) : Prop := ¬ (r a a).
+
+notation `δ` := delta.
+
+theorem delta_aux : ¬ (δ (i delta))
+         := assume H : δ (i delta),
+            H (subst (symm retract) H).
+
+check delta_aux.
\ No newline at end of file