diff --git a/tests/lean/run/decidable.lean b/tests/lean/run/decidable.lean
index a72f5686b..f2a450a7e 100644
--- a/tests/lean/run/decidable.lean
+++ b/tests/lean/run/decidable.lean
@@ -1,11 +1,7 @@
-import standard unit decidable
+import standard unit decidable if
 using bit unit decidable
 
 variables a b c : bit
 variables u v : unit
-
-theorem tst : decidable ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true)
-
-(*
-print(get_env():find("tst"):value())
-*)
+set_option pp.implicit true
+check if ((a = b) ∧ (b = c) → ¬ (u = v) ∨ (a = c) → (a = c) ↔ a = '1 ↔ true) then a else b