diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 5e3c051945..3bad872d97 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -15,7 +15,7 @@ These might not hold constructively in some applications, but we can define addi
 with both < and ≤ as needed.
 -/
 
-import logic.eq
+import logic.eq logic.connectives
 import data.unit data.sigma data.prod
 import algebra.function algebra.binary
 
diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean
index b847493024..8ccbcc62d8 100644
--- a/library/algebra/ring.lean
+++ b/library/algebra/ring.lean
@@ -9,7 +9,7 @@ Structures with multiplicative and additive components, including semirings, rin
 The development is modeled after Isabelle's library.
 -/
 
-import logic.eq data.unit data.sigma data.prod
+import logic.eq logic.connectives data.unit data.sigma data.prod
 import algebra.function algebra.binary algebra.group
 
 open eq eq.ops
diff --git a/library/data/fin.lean b/library/data/fin.lean
index 667b449e87..cfe42f86b4 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -79,6 +79,6 @@ namespace fin
   have aux₂ : to_nat (lift (of_nat_core p) (n - succ p)) = p, from calc
     to_nat (lift (of_nat_core p) (n - succ p)) = to_nat (of_nat_core p) : to_nat.lift
                                          ...   = p                      : to_nat.of_nat_core,
-  heq.to_eq (heq.trans aux₁ (heq.from_eq aux₂))
+  heq.to_eq (heq.trans aux₁ (heq.of_eq aux₂))
 
 end fin
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 7d2a2977f9..c1778ceaae 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -885,17 +885,15 @@ theorem mul_cancel_right {a b c : ℤ} (H1 : c ≠ 0) (H2 : a * c = b * c) : a =
 or.resolve_right (mul_cancel_right_or H2) H1
 
 theorem mul_ne_zero {a b : ℤ} (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
-not_intro
-  (assume H : a * b = 0,
-    or.elim (mul_eq_zero H)
-      (assume H2 : a = 0, absurd H2 Ha)
-      (assume H2 : b = 0, absurd H2 Hb))
+(assume H : a * b = 0,
+  or.elim (mul_eq_zero H)
+    (assume H2 : a = 0, absurd H2 Ha)
+    (assume H2 : b = 0, absurd H2 Hb))
 
 theorem mul_ne_zero_left {a b : ℤ} (H : a * b ≠ 0) : a ≠ 0 :=
-not_intro
-  (assume H2 : a = 0,
-    have H3 : a * b = 0, by simp,
-    absurd H3 H)
+(assume H2 : a = 0,
+  have H3 : a * b = 0, by simp,
+  absurd H3 H)
 
 theorem mul_ne_zero_right {a b : ℤ} (H : a * b ≠ 0) : b ≠ 0 :=
 mul_ne_zero_left (mul_comm a b ▸ H)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 81cfb34033..4140d68205 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -221,19 +221,18 @@ exists_intro n H2
 -- -- ### basic facts
 
 theorem lt_irrefl (a : ℤ) : ¬ a < a :=
-not_intro
-  (assume H : a < a,
-    obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
-    have H2 : a + succ n = a + 0, from
-      calc
-        a + succ n = a : Hn
-          ... = a + 0 : by simp,
-    have H3 : succ n = 0, from add_cancel_left H2,
-    have H4 : succ n = 0, from of_nat_inj H3,
-    absurd H4 !succ_ne_zero)
+(assume H : a < a,
+  obtain (n : ℕ) (Hn : a + succ n = a), from lt_elim H,
+  have H2 : a + succ n = a + 0, from
+    calc
+      a + succ n = a : Hn
+        ... = a + 0 : by simp,
+  have H3 : succ n = 0, from add_cancel_left H2,
+  have H4 : succ n = 0, from of_nat_inj H3,
+  absurd H4 !succ_ne_zero)
 
 theorem lt_imp_ne {a b : ℤ} (H : a < b) : a ≠ b :=
-not_intro (assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b))
+(assume H2 : a = b, absurd (H2 ▸ H) (lt_irrefl b))
 
 theorem lt_of_nat (n m : ℕ) : (of_nat n < of_nat m) ↔ (n < m) :=
 calc
@@ -284,10 +283,10 @@ theorem lt_trans {a b c : ℤ} (H1 : a < b) (H2 : b < c) : a < c :=
 lt_le_trans H1 (lt_imp_le H2)
 
 theorem le_imp_not_gt {a b : ℤ} (H : a ≤ b) : ¬ a > b :=
-not_intro (assume H2 : a > b, absurd (le_lt_trans H H2) (lt_irrefl a))
+(assume H2 : a > b, absurd (le_lt_trans H H2) (lt_irrefl a))
 
 theorem lt_imp_not_ge {a b : ℤ} (H : a < b) : ¬ a ≥ b :=
-not_intro (assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt_irrefl a))
+(assume H2 : a ≥ b, absurd (lt_le_trans H H2) (lt_irrefl a))
 
 theorem lt_antisym {a b : ℤ} (H : a < b) : ¬ b < a :=
 le_imp_not_gt (lt_imp_le H)
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index eea1177aed..256a4a472f 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -4,7 +4,7 @@
 
 -- Basic operations on the natural numbers.
 
-import data.num algebra.binary
+import logic.connectives data.num algebra.binary
 
 open eq.ops binary
 
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 2ac912b135..df5255bcc1 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -54,10 +54,9 @@ obtain (k : ℕ) (Hk : n + k = 0), from le_elim H,
 add.eq_zero_left Hk
 
 theorem not_succ_zero_le (n : ℕ) : ¬ succ n ≤ 0 :=
-not_intro
-  (assume H : succ n ≤ 0,
-    have H2 : succ n = 0, from le_zero H,
-    absurd H2 !succ_ne_zero)
+(assume H : succ n ≤ 0,
+  have H2 : succ n = 0, from le_zero H,
+  absurd H2 !succ_ne_zero)
 
 theorem le_trans {n m k : ℕ} (H1 : n ≤ m) (H2 : m ≤ k) : n ≤ k :=
 le.trans H1 H2
@@ -249,7 +248,7 @@ theorem lt_imp_ne {n m : ℕ} (H : n < m) : n ≠ m :=
 λ heq : n = m, absurd H (heq ▸ !lt.irrefl)
 
 theorem lt_irrefl (n : ℕ) : ¬ n < n :=
-not_intro (assume H : n < n, absurd rfl (lt_imp_ne H))
+(assume H : n < n, absurd rfl (lt_imp_ne H))
 
 theorem lt_def (n m : ℕ) : n < m ↔ succ n ≤ m :=
 iff.intro
@@ -287,7 +286,7 @@ le.rec_on H
   (λ m (h : n < m), lt.asymm h)
 
 theorem lt_imp_not_ge {n m : ℕ} (H : n < m) : ¬ n ≥ m :=
-not_intro (assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
+(assume H2 : m ≤ n, absurd (lt.of_lt_of_le H H2) !lt_irrefl)
 
 theorem lt_antisym {n m : ℕ} (H : n < m) : ¬ m < n :=
 lt.asymm H
diff --git a/library/data/sigma/thms.lean b/library/data/sigma/thms.lean
index 6309da403d..8728c2c1e0 100644
--- a/library/data/sigma/thms.lean
+++ b/library/data/sigma/thms.lean
@@ -54,7 +54,7 @@ namespace sigma
   theorem ndtrip_eq {A B : Type} {C : A → B → Type} {a₁ a₂ : A} {b₁ b₂ : B}
       {c₁ : C a₁ b₁} {c₂ : C a₂ b₂} (H₁ : a₁ = a₂) (H₂ : b₁ = b₂)
       (H₃ : cast (congr_arg2 C H₁ H₂) c₁ = c₂) : ⟨a₁, b₁, c₁⟩ = ⟨a₂, b₂, c₂⟩ :=
-  hdcongr_arg3 dtrip H₁ (heq.from_eq H₂) H₃
+  hdcongr_arg3 dtrip H₁ (heq.of_eq H₂) H₃
 
   theorem ndtrip_equal {A B : Type} {C : A → B → Type} {p₁ p₂ : Σa b, C a b} :
       ∀(H₁ : dpr1 p₁ = dpr1 p₂) (H₂ : dpr2' p₁ = dpr2' p₂)
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 0f355b316a..56c1f4b58c 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -7,6 +7,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 The sum type, aka disjoint union.
 -/
+import logic.connectives
 open inhabited decidable eq.ops
 
 namespace sum
@@ -48,13 +49,13 @@ namespace sum
               (assume Hne : a₁ ≠ a₂, decidable.inr (mt inl_inj Hne)))
           (take b₂,
             have H₃ : (inl B a₁ = inr A b₂) ↔ false,
-              from iff.intro inl_neq_inr (assume H₄, false_elim H₄),
+              from iff.intro inl_neq_inr (assume H₄, !false.rec H₄),
             show decidable (inl B a₁ = inr A b₂), from decidable_iff_equiv _ (iff.symm H₃)))
       (take b₁, show decidable (inr A b₁ = s₂), from
         rec_on s₂
           (take a₂,
             have H₃ : (inr A b₁ = inl B a₂) ↔ false,
-              from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, false_elim H₄),
+              from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, !false.rec H₄),
             show decidable (inr A b₁ = inl B a₂), from decidable_iff_equiv _ (iff.symm H₃))
           (take b₂, show decidable (inr A b₁ = inr A b₂), from
             decidable.rec_on (H₂ b₁ b₂)
diff --git a/library/init/logic.lean b/library/init/logic.lean
index 0f6b3ebae9..25edd80a6d 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -10,12 +10,6 @@ import init.datatypes init.reserved_notation
 -- implication
 -- -----------
 
-definition imp (a b : Prop) : Prop := a → b
-
--- make c explicit and rename to false.elim
-theorem false_elim {c : Prop} (H : false) : c :=
-false.rec c H
-
 definition trivial := true.intro
 
 definition not (a : Prop) := a → false
@@ -24,28 +18,12 @@ prefix `¬` := not
 definition absurd {a : Prop} {b : Type} (H1 : a) (H2 : ¬a) : b :=
 false.rec b (H2 H1)
 
-theorem mt {a b : Prop} (H1 : a → b) (H2 : ¬b) : ¬a :=
-assume Ha : a, absurd (H1 Ha) H2
-
 -- not
 -- ---
 
 theorem not_false : ¬false :=
 assume H : false, H
 
-theorem not_not_intro {a : Prop} (Ha : a) : ¬¬a :=
-assume Hna : ¬a, absurd Ha Hna
-
-theorem not_intro {a : Prop} (H : a → false) : ¬a := H
-
-theorem not_elim {a : Prop} (H1 : ¬a) (H2 : a) : false := H1 H2
-
-theorem not_implies_left {a b : Prop} (H : ¬(a → b)) : ¬¬a :=
-assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
-
-theorem not_implies_right {a b : Prop} (H : ¬(a → b)) : ¬b :=
-assume Hb : b, absurd (assume Ha : a, Hb) H
-
 -- eq
 -- --
 
@@ -60,15 +38,6 @@ namespace eq
   variables {A : Type}
   variables {a b c a': A}
 
-  definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
-  eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
-
-  theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
-  rfl
-
-  theorem irrel (H₁ H₂ : a = b) : H₁ = H₂ :=
-  !proof_irrel
-
   theorem subst {P : A → Prop} (H₁ : a = b) (H₂ : P a) : P b :=
   rec H₂ H₁
 
@@ -154,37 +123,31 @@ namespace heq
   definition elim {A : Type} {a : A} {P : A → Type} {b : A} (H₁ : a == b) (H₂ : P a) : P b :=
   eq.rec_on (to_eq H₁) H₂
 
-  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
-  rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
-
   theorem subst {P : ∀T : Type, T → Prop} (H₁ : a == b) (H₂ : P A a) : P B b :=
   rec_on H₁ H₂
 
   theorem symm (H : a == b) : b == a :=
   rec_on H (refl a)
 
-  definition type_eq (H : a == b) : A = B :=
-  heq.rec_on H (eq.refl A)
-
-  theorem from_eq (H : a = a') : a == a' :=
+  theorem of_eq (H : a = a') : a == a' :=
   eq.subst H (refl a)
 
   theorem trans (H₁ : a == b) (H₂ : b == c) : a == c :=
   subst H₂ H₁
 
-  theorem trans_left (H₁ : a == b) (H₂ : b = b') : a == b' :=
-  trans H₁ (from_eq H₂)
+  theorem of_heq_of_eq (H₁ : a == b) (H₂ : b = b') : a == b' :=
+  trans H₁ (of_eq H₂)
 
-  theorem trans_right (H₁ : a = a') (H₂ : a' == b) : a == b :=
-  trans (from_eq H₁) H₂
+  theorem of_eq_of_heq (H₁ : a = a') (H₂ : a' == b) : a == b :=
+  trans (of_eq H₁) H₂
 
   theorem true_elim {a : Prop} (H : a == true) : a :=
   eq.true_elim (heq.to_eq H)
 end heq
 
 calc_trans heq.trans
-calc_trans heq.trans_left
-calc_trans heq.trans_right
+calc_trans heq.of_heq_of_eq
+calc_trans heq.of_eq_of_heq
 calc_symm  heq.symm
 
 -- and
@@ -199,23 +162,11 @@ namespace and
   theorem elim (H₁ : a ∧ b) (H₂ : a → b → c) : c :=
   rec H₂ H₁
 
-  theorem swap (H : a ∧ b) : b ∧ a :=
-  intro (elim_right H) (elim_left H)
-
   definition not_left (b : Prop) (Hna : ¬a) : ¬(a ∧ b) :=
   assume H : a ∧ b, absurd (elim_left H) Hna
 
   definition not_right (a : Prop) {b : Prop} (Hnb : ¬b) : ¬(a ∧ b) :=
   assume H : a ∧ b, absurd (elim_right H) Hnb
-
-  theorem imp_and (H₁ : a ∧ b) (H₂ : a → c) (H₃ : b → d) : c ∧ d :=
-  elim H₁ (assume Ha : a, assume Hb : b, intro (H₂ Ha) (H₃ Hb))
-
-  theorem imp_left (H₁ : a ∧ c) (H : a → b) : b ∧ c :=
-  elim H₁ (assume Ha : a, assume Hc : c, intro (H Ha) Hc)
-
-  theorem imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
-  elim H₁ (assume Hc : c, assume Ha : a, intro Hc (H Ha))
 end and
 
 -- or
@@ -233,45 +184,12 @@ namespace or
   theorem elim (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → c) : c :=
   rec H₂ H₃ H₁
 
-  theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
-  elim H Ha (assume H₂, elim H₂ Hb Hc)
-
-  theorem resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b :=
-  elim H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb)
-
-  theorem resolve_left (H₁ : a ∨ b) (H₂ : ¬b) : a :=
-  elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
-
-  theorem swap (H : a ∨ b) : b ∨ a :=
-  elim H (assume Ha, inr Ha) (assume Hb, inl Hb)
-
   definition not_intro (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b) :=
   assume H : a ∨ b, or.rec_on H
     (assume Ha, absurd Ha Hna)
     (assume Hb, absurd Hb Hnb)
-
-  theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d :=
-  elim H₁
-    (assume Ha : a, inl (H₂ Ha))
-    (assume Hb : b, inr (H₃ Hb))
-
-  theorem imp_or_left (H₁ : a ∨ c) (H : a → b) : b ∨ c :=
-  elim H₁
-    (assume H₂ : a, inl (H H₂))
-    (assume H₂ : c, inr H₂)
-
-  theorem imp_or_right (H₁ : c ∨ a) (H : a → b) : c ∨ b :=
-  elim H₁
-    (assume H₂ : c, inl H₂)
-    (assume H₂ : a, inr (H H₂))
 end or
 
-theorem not_not_em {p : Prop} : ¬¬(p ∨ ¬p) :=
-assume not_em : ¬(p ∨ ¬p),
-  have Hnp : ¬p, from
-    assume Hp : p, absurd (or.inl Hp) not_em,
-  absurd (or.inr Hnp) not_em
-
 -- iff
 -- ---
 definition iff (a b : Prop) := (a → b) ∧ (b → a)
@@ -280,9 +198,6 @@ notation a <-> b := iff a b
 notation a ↔ b := iff a b
 
 namespace iff
-  definition def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
-  rfl
-
   definition intro (H₁ : a → b) (H₂ : b → a) : a ↔ b :=
   and.intro H₁ H₂
 
@@ -299,8 +214,8 @@ namespace iff
 
   definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b :=
   intro
-    (assume Hna, mt (elim_right H₁) Hna)
-    (assume Hnb, mt (elim_left H₁) Hnb)
+    (assume (Hna : ¬ a) (Hb : b), absurd (elim_right H₁ Hb) Hna)
+    (assume (Hnb : ¬ b) (Ha : a), absurd (elim_left H₁ Ha) Hnb)
 
   definition refl (a : Prop) : a ↔ a :=
   intro (assume H, H) (assume H, H)
@@ -332,40 +247,6 @@ end iff
 calc_refl iff.refl
 calc_trans iff.trans
 
--- comm and assoc for and / or
--- ---------------------------
-namespace and
-  theorem comm : a ∧ b ↔ b ∧ a :=
-  iff.intro (λH, swap H) (λH, swap H)
-
-  theorem assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
-  iff.intro
-    (assume H, intro
-      (elim_left (elim_left H))
-      (intro (elim_right (elim_left H)) (elim_right H)))
-    (assume H, intro
-      (intro (elim_left H) (elim_left (elim_right H)))
-      (elim_right (elim_right H)))
-end and
-
-namespace or
-  theorem comm : a ∨ b ↔ b ∨ a :=
-  iff.intro (λH, swap H) (λH, swap H)
-
-  theorem assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
-  iff.intro
-    (assume H, elim H
-      (assume H₁, elim H₁
-        (assume Ha, inl Ha)
-        (assume Hb, inr (inl Hb)))
-      (assume Hc, inr (inr Hc)))
-    (assume H, elim H
-      (assume Ha, (inl (inl Ha)))
-      (assume H₁, elim H₁
-        (assume Hb, inl (inr Hb))
-        (assume Hc, inr Hc)))
-end or
-
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 intro : ∀ (a : A), P a → Exists P
 
@@ -377,24 +258,10 @@ notation `∃` binders `,` r:(scoped P, Exists P) := r
 theorem exists_elim {A : Type} {p : A → Prop} {B : Prop} (H1 : ∃x, p x) (H2 : ∀ (a : A) (H : p a), B) : B :=
 Exists.rec H2 H1
 
-definition exists_unique {A : Type} (p : A → Prop) :=
-∃x, p x ∧ ∀y, p y → y = x
-
-notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
-
-theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : ∃!x, p x :=
-exists_intro w (and.intro H1 H2)
-
-theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
-                           (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
-obtain w Hw, from H2,
-H1 w (and.elim_left Hw) (and.elim_right Hw)
-
 inductive decidable [class] (p : Prop) : Type :=
 inl :  p → decidable p,
 inr : ¬p → decidable p
 
-
 definition true.decidable [instance] : decidable true :=
 decidable.inl trivial
 
@@ -406,7 +273,7 @@ namespace decidable
 
   definition rec_on_true [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : p) (H4 : H1 H3)
       : rec_on H H1 H2 :=
-  rec_on H (λh, H4) (λh, false.rec _ (h H3))
+  rec_on H (λh, H4) (λh, !false.rec (h H3))
 
   definition rec_on_false [H : decidable p] {H1 : p → Type} {H2 : ¬p → Type} (H3 : ¬p) (H4 : H2 H3)
       : rec_on H H1 H2 :=
@@ -421,7 +288,7 @@ namespace decidable
   theorem by_contradiction [Hp : decidable p] (H : ¬p → false) : p :=
   by_cases
     (assume H1 : p, H1)
-    (assume H1 : ¬p, false_elim (H H1))
+    (assume H1 : ¬p, false.rec _ (H H1))
 
   definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q :=
   rec_on Hp
@@ -452,7 +319,7 @@ section
 
   definition not.decidable [instance] (Hp : decidable p) : decidable (¬p) :=
   rec_on Hp
-    (assume Hp,  inr (not_not_intro Hp))
+    (assume Hp,  inr (λ Hnp, absurd Hp Hnp))
     (assume Hnp, inl Hnp)
 
   definition implies.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p → q) :=
@@ -577,13 +444,13 @@ definition is_false (c : Prop) [H : decidable c] : Prop :=
 if c then false else true
 
 theorem of_is_true {c : Prop} [H₁ : decidable c] (H₂ : is_true c) : c :=
-decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, false_elim (if_neg Hnc ▸ H₂))
+decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, !false.rec (if_neg Hnc ▸ H₂))
 
 theorem not_of_not_is_true {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_true c) : ¬ c :=
 decidable.rec_on H₁ (λ Hc, absurd true.intro (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
 
 theorem not_of_is_false {c : Prop} [H₁ : decidable c] (H₂ : is_false c) : ¬ c :=
-decidable.rec_on H₁ (λ Hc, false_elim (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
+decidable.rec_on H₁ (λ Hc, !false.rec (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
 
 theorem of_not_is_false {c : Prop} [H₁ : decidable c] (H₂ : ¬ is_false c) : c :=
 decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd true.intro (if_neg Hnc ▸ H₂))
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 6dfa78d6ee..cbdc55a5ed 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -6,7 +6,7 @@ Module: logic.axims.classical
 Author: Leonardo de Moura
 -/
 
-import logic.quantifiers logic.cast algebra.relation
+import logic.connectives logic.quantifiers logic.cast algebra.relation
 
 open eq.ops
 
diff --git a/library/logic/cast.lean b/library/logic/cast.lean
index cbb4a7fc09..396ef4c634 100644
--- a/library/logic/cast.lean
+++ b/library/logic/cast.lean
@@ -27,6 +27,12 @@ namespace heq
   universe variable u
   variables {A B C : Type.{u}} {a a' : A} {b b' : B} {c : C}
 
+  definition type_eq (H : a == b) : A = B :=
+  heq.rec_on H (eq.refl A)
+
+  theorem drec_on {C : Π {B : Type} (b : B), a == b → Type} (H₁ : a == b) (H₂ : C a (refl a)) : C b H₁ :=
+  rec (λ H₁ : a == a, show C a H₁, from H₂) H₁ H₁
+
   theorem to_cast_eq (H : a == b) : cast (type_eq H) a = b :=
   drec_on H !cast_eq
 end heq
@@ -106,7 +112,7 @@ section
 
   theorem cast_app (H : P = P') (f : Π x, P x) (a : A) : cast (pi_eq H) f a == f a :=
   have H₁ : ∀ (H : (Π x, P x) = (Π x, P x)), cast H f a == f a, from
-    assume H, heq.from_eq (congr_fun (cast_eq H f) a),
+    assume H, heq.of_eq (congr_fun (cast_eq H f) a),
   have H₂ : ∀ (H : (Π x, P x) = (Π x, P' x)), cast H f a == f a, from
     H ▸ H₁,
   H₂ (pi_eq H)
diff --git a/library/logic/connectives.lean b/library/logic/connectives.lean
new file mode 100644
index 0000000000..51ddd89761
--- /dev/null
+++ b/library/logic/connectives.lean
@@ -0,0 +1,138 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Jeremy Avigad, Leonardo de Moura
+
+definition imp (a b : Prop) : Prop := a → b
+
+variables {a b c d : Prop}
+
+theorem mt (H1 : a → b) (H2 : ¬b) : ¬a :=
+assume Ha : a, absurd (H1 Ha) H2
+
+-- make c explicit and rename to false.elim
+theorem false_elim {c : Prop} (H : false) : c :=
+false.rec c H
+
+-- not
+-- ---
+
+theorem not_elim (H1 : ¬a) (H2 : a) : false := H1 H2
+
+theorem not_intro (H : a → false) : ¬a := H
+
+theorem not_not_intro (Ha : a) : ¬¬a :=
+assume Hna : ¬a, absurd Ha Hna
+
+theorem not_implies_left (H : ¬(a → b)) : ¬¬a :=
+assume Hna : ¬a, absurd (assume Ha : a, absurd Ha Hna) H
+
+theorem not_implies_right (H : ¬(a → b)) : ¬b :=
+assume Hb : b, absurd (assume Ha : a, Hb) H
+
+theorem not_not_em : ¬¬(a ∨ ¬a) :=
+assume not_em : ¬(a ∨ ¬a),
+  have Hnp : ¬a, from
+    assume Hp : a, absurd (or.inl Hp) not_em,
+  absurd (or.inr Hnp) not_em
+
+-- and
+-- ---
+
+namespace and
+  theorem swap (H : a ∧ b) : b ∧ a :=
+  intro (elim_right H) (elim_left H)
+
+  theorem imp_and (H₁ : a ∧ b) (H₂ : a → c) (H₃ : b → d) : c ∧ d :=
+  elim H₁ (assume Ha : a, assume Hb : b, intro (H₂ Ha) (H₃ Hb))
+
+  theorem imp_left (H₁ : a ∧ c) (H : a → b) : b ∧ c :=
+  elim H₁ (assume Ha : a, assume Hc : c, intro (H Ha) Hc)
+
+  theorem imp_right (H₁ : c ∧ a) (H : a → b) : c ∧ b :=
+  elim H₁ (assume Hc : c, assume Ha : a, intro Hc (H Ha))
+
+  theorem comm : a ∧ b ↔ b ∧ a :=
+  iff.intro (λH, swap H) (λH, swap H)
+
+  theorem assoc : (a ∧ b) ∧ c ↔ a ∧ (b ∧ c) :=
+  iff.intro
+    (assume H, intro
+      (elim_left (elim_left H))
+      (intro (elim_right (elim_left H)) (elim_right H)))
+    (assume H, intro
+      (intro (elim_left H) (elim_left (elim_right H)))
+      (elim_right (elim_right H)))
+end and
+
+-- or
+-- --
+
+namespace or
+  theorem imp_or (H₁ : a ∨ b) (H₂ : a → c) (H₃ : b → d) : c ∨ d :=
+  elim H₁
+    (assume Ha : a, inl (H₂ Ha))
+    (assume Hb : b, inr (H₃ Hb))
+
+  theorem imp_or_left (H₁ : a ∨ c) (H : a → b) : b ∨ c :=
+  elim H₁
+    (assume H₂ : a, inl (H H₂))
+    (assume H₂ : c, inr H₂)
+
+  theorem imp_or_right (H₁ : c ∨ a) (H : a → b) : c ∨ b :=
+  elim H₁
+    (assume H₂ : c, inl H₂)
+    (assume H₂ : a, inr (H H₂))
+
+  theorem elim3 (H : a ∨ b ∨ c) (Ha : a → d) (Hb : b → d) (Hc : c → d) : d :=
+  elim H Ha (assume H₂, elim H₂ Hb Hc)
+
+  theorem resolve_right (H₁ : a ∨ b) (H₂ : ¬a) : b :=
+  elim H₁ (assume Ha, absurd Ha H₂) (assume Hb, Hb)
+
+  theorem resolve_left (H₁ : a ∨ b) (H₂ : ¬b) : a :=
+  elim H₁ (assume Ha, Ha) (assume Hb, absurd Hb H₂)
+
+  theorem swap (H : a ∨ b) : b ∨ a :=
+  elim H (assume Ha, inr Ha) (assume Hb, inl Hb)
+
+  theorem comm : a ∨ b ↔ b ∨ a :=
+  iff.intro (λH, swap H) (λH, swap H)
+
+  theorem assoc : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) :=
+  iff.intro
+    (assume H, elim H
+      (assume H₁, elim H₁
+        (assume Ha, inl Ha)
+        (assume Hb, inr (inl Hb)))
+      (assume Hc, inr (inr Hc)))
+    (assume H, elim H
+      (assume Ha, (inl (inl Ha)))
+      (assume H₁, elim H₁
+        (assume Hb, inl (inr Hb))
+        (assume Hc, inr Hc)))
+end or
+
+-- iff
+-- ---
+
+namespace iff
+  definition def : (a ↔ b) = ((a → b) ∧ (b → a)) :=
+  !eq.refl
+
+end iff
+
+-- exists_unique
+-- -------------
+
+definition exists_unique {A : Type} (p : A → Prop) :=
+∃x, p x ∧ ∀y, p y → y = x
+
+notation `∃!` binders `,` r:(scoped P, exists_unique P) := r
+
+theorem exists_unique_intro {A : Type} {p : A → Prop} (w : A) (H1 : p w) (H2 : ∀y, p y → y = w) : ∃!x, p x :=
+exists_intro w (and.intro H1 H2)
+
+theorem exists_unique_elim {A : Type} {p : A → Prop} {b : Prop}
+                           (H2 : ∃!x, p x) (H1 : ∀x, p x → (∀y, p y → y = x) → b) : b :=
+obtain w Hw, from H2,
+H1 w (and.elim_left Hw) (and.elim_right Hw)
diff --git a/library/logic/default.lean b/library/logic/default.lean
index 3f3114f9e0..4d5618f4f9 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -2,5 +2,5 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.eq logic.cast logic.subsingleton
+import logic.eq logic.connectives logic.cast logic.subsingleton
 import logic.quantifiers logic.instances logic.identities
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 5491c007ca..db73877439 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -15,6 +15,16 @@ open eq.ops
 
 namespace eq
   variables {A B : Type} {a a' a₁ a₂ a₃ a₄ : A}
+
+  theorem irrel (H₁ H₂ : a = a') : H₁ = H₂ :=
+  !proof_irrel
+
+  theorem id_refl (H₁ : a = a) : H₁ = (eq.refl a) :=
+  rfl
+
+  definition drec_on {B : Πa' : A, a = a' → Type} (H₁ : a = a') (H₂ : B a (refl a)) : B a' H₁ :=
+  eq.rec (λH₁ : a = a, show B a H₁, from H₂) H₁ H₁
+
   theorem rec_on_id {B : A → Type} (H : a = a) (b : B a) : rec_on H b = b :=
   rfl
 
diff --git a/library/logic/identities.lean b/library/logic/identities.lean
index 7cc97b1d34..7dfd7754c2 100644
--- a/library/logic/identities.lean
+++ b/library/logic/identities.lean
@@ -8,7 +8,7 @@
 -- Useful logical identities. In the absence of propositional extensionality, some of the
 -- calculations use the type class support provided by logic.instances
 
-import logic.instances logic.quantifiers logic.cast
+import logic.connectives logic.instances logic.quantifiers logic.cast
 
 open relation decidable relation.iff_ops
 
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index c5b36b990c..44d1ebee75 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -8,7 +8,7 @@ Author: Jeremy Avigad
 Class instances for iff and eq.
 -/
 
-import algebra.relation
+import logic.connectives algebra.relation
 
 namespace relation
 
diff --git a/tests/lean/interactive/findp.input.expected.out b/tests/lean/interactive/findp.input.expected.out
index a7644b6778..72f2e1c2c4 100644
--- a/tests/lean/interactive/findp.input.expected.out
+++ b/tests/lean/interactive/findp.input.expected.out
@@ -3,7 +3,6 @@
 -- BEGINFINDP STALE
 false|Prop
 false.rec|Π (C : Type), false → C
-false_elim|false → ?c
 false.of_ne|?a ≠ ?a → false
 false.rec_on|Π (C : Type), false → C
 false.cases_on|Π (C : Type), false → C
diff --git a/tests/lean/run/pquot.lean b/tests/lean/run/pquot.lean
index 1ec4a19ff7..553e32abe8 100644
--- a/tests/lean/run/pquot.lean
+++ b/tests/lean/run/pquot.lean
@@ -55,7 +55,7 @@ definition pquot.lift {A : Type} {R : A → A → Prop} {B : Type}
                       (sound : ∀ (a b : A), R a b → f a = f b)
                       (q : pquot R)
                       : B :=
-pquot.rec_on q f (λ (a b : A) (H : R a b), heq.from_eq (sound a b H))
+pquot.rec_on q f (λ (a b : A) (H : R a b), heq.of_eq (sound a b H))
 
 theorem pquot.induction_on {A : Type} {R : A → A → Prop} {P : pquot R → Prop}
                            (q : pquot R)
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index 9b6be639e2..1da2e9628e 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -1,6 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
+import logic
 open inhabited decidable
 namespace play
 -- TODO: take this outside the namespace when the inductive package handles it better