diff --git a/tests/lean/interactive/t3.lean b/tests/lean/interactive/t3.lean
new file mode 100644
index 000000000..37ca5de17
--- /dev/null
+++ b/tests/lean/interactive/t3.lean
@@ -0,0 +1,9 @@
+Theorem T2 (a b : Bool) : b => a \/ b.
+apply imp_tactic.
+apply disj_tactic.
+back.
+back.
+apply assumption_tactic.
+done.
+
+Show Environment 1.
\ No newline at end of file
diff --git a/tests/lean/interactive/t3.lean.expected.out b/tests/lean/interactive/t3.lean.expected.out
new file mode 100644
index 000000000..eac4ac983
--- /dev/null
+++ b/tests/lean/interactive/t3.lean.expected.out
@@ -0,0 +1,19 @@
+Type Ctrl-D or 'Exit.' to exit or 'Help.' for help.
+#   Set: pp::colors
+  Set: pp::unicode
+Proof state:
+a : Bool, b : Bool ⊢ b ⇒ a ∨ b
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ a ∨ b
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ a
+## Proof state:
+H : b, a : Bool, b : Bool ⊢ b
+## Error (line: 8, pos: 0) failed to backtrack
+Proof state:
+H : b, a : Bool, b : Bool ⊢ b
+## Proof state:
+no goals
+##   Proved: T2
+# Theorem T2 (a b : Bool) : b ⇒ a ∨ b := Discharge (λ H : b, Disj2 a H)
+# 
\ No newline at end of file