From 7cd15aaecdd14cad47bd313229d20476be2c7ea9 Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Mon, 16 Nov 2015 17:47:18 -0800
Subject: [PATCH] test(simplifier11): add necessary simp rule

---
 tests/lean/simplifier11.lean | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/tests/lean/simplifier11.lean b/tests/lean/simplifier11.lean
index 4f14e25c2c..877714c92a 100644
--- a/tests/lean/simplifier11.lean
+++ b/tests/lean/simplifier11.lean
@@ -1,9 +1,8 @@
 -- Conditional congruence
 import logic.connectives logic.quantifiers
 
--- TODO(dhs): either add this to the library or add a `ceqv` rule for
--- ¬ c ==> (¬ c ↔ true) in addition to (c ↔ false)
-lemma not_workaround [simp] : ∀ (P : Prop), (P ↔ false) → (¬ P ↔ true) := sorry
+-- TODO(dhs): add this to the library
+lemma not_false_true [simp] : (¬ false) ↔ true := sorry
 
 namespace if_congr
 constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
@@ -32,7 +31,6 @@ attribute h_e [simp]
 attribute if_ctx_simp_congr [congr]
 
 #simplify eq env 0 (ite b x y)
-
 end if_ctx_simp_congr
 
 namespace if_congr_prop