diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index 21d2f7be73..9dee8a3b8c 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -500,11 +500,19 @@ struct app_builder::imp {
     }
 
     expr mk_not_of_iff_false(expr const & H) {
+        if (is_constant(get_app_fn(H), get_iff_false_intro_name())) {
+            // not_of_iff_false (iff_false_intro H) == H
+            return app_arg(H);
+        }
         // TODO(Leo): implement custom version if bottleneck.
         return mk_app(get_not_of_iff_false_name(), {H});
     }
 
     expr mk_of_iff_true(expr const & H) {
+        if (is_constant(get_app_fn(H), get_iff_true_intro_name())) {
+            // of_iff_true (iff_true_intro H) == H
+            return app_arg(H);
+        }
         // TODO(Leo): implement custom version if bottleneck.
         return mk_app(get_of_iff_true_name(), {H});
     }
diff --git a/tests/lean/run/blast_cc12.lean b/tests/lean/run/blast_cc12.lean
index 4cc5248497..6640000d2f 100644
--- a/tests/lean/run/blast_cc12.lean
+++ b/tests/lean/run/blast_cc12.lean
@@ -1,5 +1,6 @@
 set_option blast.subst false
 set_option blast.simp false
+set_option pp.all true
 
 definition foo1 (a b : nat) (p : Prop) : a = b → (b = a → p) → p :=
 by blast
@@ -10,3 +11,8 @@ definition foo2 (a b c : nat) (p : Prop) : a = b → b = c → (c = a → p) →
 by blast
 
 print foo2
+
+definition foo3 (a b c d : nat) (p : Prop) : a ≠ d → (d ≠ a → p) → p :=
+by blast
+
+print foo3