From 76f989d51c2d377a473dc155d39d525f3c8a60e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Mar 2017 09:50:01 -0800
Subject: [PATCH] chore(library/init/data/bool/lemmas): add (coe tt) and (coe
 ff) simp lemmas

---
 library/init/data/bool/lemmas.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/library/init/data/bool/lemmas.lean b/library/init/data/bool/lemmas.lean
index 8a4f3dc328..da0bbd7df2 100644
--- a/library/init/data/bool/lemmas.lean
+++ b/library/init/data/bool/lemmas.lean
@@ -88,3 +88,9 @@ by cases a; cases b; simp
 
 @[simp] lemma bnot_eq_ff_eq_eq_tt (a : bool) : (bnot a = ff) = (a = tt) :=
 by cases a; simp
+
+@[simp] lemma coe_ff : ↑ff = false :=
+show (ff = tt) = false, by simp
+
+@[simp] lemma coe_tt : ↑tt = true :=
+show (tt = tt) = true, by simp