diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index 4ffb70e7f6..a7644b6778 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -11,9 +11,12 @@ false.decidable|decidable false
 false.induction_on|∀ (C : Prop), false → C
 true_ne_false|¬ true = false
 eq.false_elim|?p = false → ¬ ?p
+not_of_is_false|is_false ?c → ¬ ?c
 p_ne_false|?p → ?p ≠ false
+is_false|Π (c : Prop) [H : decidable c], Prop
 decidable.rec_on_false|Π (H3 : ¬ ?p), ?H2 H3 → decidable.rec_on ?H ?H1 ?H2
 not_false|¬ false
+of_not_is_false|¬ is_false ?c → ?c
 if_false|∀ (t e : ?A), ite false t e = e
 iff.false_elim|?a ↔ false → ¬ ?a
 -- ENDFINDP