From 3650ffdd4f2971e9cf18a593285e1ce7d2a47c9e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 30 Jun 2014 00:29:42 -0700 Subject: [PATCH] feat(library/standard): add iff_mp_right and iff_mp_left Signed-off-by: Leonardo de Moura --- library/standard/logic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/standard/logic.lean b/library/standard/logic.lean index eb779e9e50..e0163d9b76 100644 --- a/library/standard/logic.lean +++ b/library/standard/logic.lean @@ -98,6 +98,12 @@ theorem iff_elim_left {a b : Bool} (H : a ↔ b) : a → b theorem iff_elim_right {a b : Bool} (H : a ↔ b) : b → a := iff_elim (assume H1 H2, H2) H +theorem iff_mp_left {a b : Bool} (H1 : a ↔ b) (H2 : a) : b +:= (iff_elim_left H1) H2 + +theorem iff_mp_right {a b : Bool} (H1 : a ↔ b) (H2 : b) : a +:= (iff_elim_right H1) H2 + inductive Exists {A : Type} (P : A → Bool) : Bool := | exists_intro : ∀ (a : A), P a → Exists P