diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index cab2dbece..5ffe46e13 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -132,7 +132,7 @@ namespace morphism
   theorem symm  ⦃a b   : ob⦄ (H  : a ≅ b)              : b ≅ a := mk (inverse (iso H))
   theorem trans ⦃a b c : ob⦄ (H1 : a ≅ b) (H2 : b ≅ c) : a ≅ c := mk (iso H2 ∘ iso H1)
   theorem is_equivalence_eq [instance] (T : Type) : is_equivalence isomorphic :=
-  is_equivalence.mk (is_reflexive.mk refl) (is_symmetric.mk symm) (is_transitive.mk trans)
+  is_equivalence.mk refl symm trans
   end isomorphic
 
   inductive is_mono [class] (f : a ⟶ b) : Prop :=
diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 16343a167..4e60c4595 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -12,178 +12,113 @@ import logic.prop
 
 namespace relation
 
-  section
-    variables {T : Type} (R : T → T → Type)
+/- properties of binary relations -/
 
-    definition reflexive : Type := ∀x, R x x
-    definition symmetric : Type := ∀⦃x y⦄, R x y → R y x
-    definition transitive : Type := ∀⦃x y z⦄, R x y → R y z → R x z
-  end
+section
+  variables {T : Type} (R : T → T → Type)
 
-inductive is_reflexive [class] {T : Type} (R : T → T → Type) : Prop :=
-mk : reflexive R → is_reflexive R
-
-namespace is_reflexive
-
-  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_reflexive R) : reflexive R :=
-  is_reflexive.rec (λu, u) C
-
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_reflexive R] : reflexive R :=
-  is_reflexive.rec (λu, u) C
-
-end is_reflexive
+  definition reflexive : Type := ∀x, R x x
+  definition symmetric : Type := ∀⦃x y⦄, R x y → R y x
+  definition transitive : Type := ∀⦃x y z⦄, R x y → R y z → R x z
+end
 
 
-inductive is_symmetric [class] {T : Type} (R : T → T → Type) : Prop :=
-mk : symmetric R → is_symmetric R
+/- classes for equivalence relations -/
 
-namespace is_symmetric
+structure is_reflexive [class] {T : Type} (R : T → T → Type) := (refl : reflexive R)
+structure is_symmetric [class] {T : Type} (R : T → T → Type) := (symm : symmetric R)
+structure is_transitive [class] {T : Type} (R : T → T → Type) := (trans : transitive R)
 
-  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_symmetric R) : symmetric R :=
-  is_symmetric.rec (λu, u) C
-
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_symmetric R] : symmetric R :=
-  is_symmetric.rec (λu, u) C
-
-end is_symmetric
-
-
-inductive is_transitive [class] {T : Type} (R : T → T → Type) : Prop :=
-mk : transitive R → is_transitive R
-
-namespace is_transitive
-
-  definition app ⦃T : Type⦄ {R : T → T → Prop} (C : is_transitive R) : transitive R :=
-  is_transitive.rec (λu, u) C
-
-  definition infer ⦃T : Type⦄ (R : T → T → Prop) [C : is_transitive R] : transitive R :=
-  is_transitive.rec (λu, u) C
-
-end is_transitive
-
-
-inductive is_equivalence [class] {T : Type} (R : T → T → Type) : Prop :=
-mk : is_reflexive R → is_symmetric R → is_transitive R → is_equivalence R
-
-theorem is_equivalence.is_reflexive [instance]
-        {T : Type} (R : T → T → Type) {C : is_equivalence R} : is_reflexive R :=
-is_equivalence.rec (λx y z, x) C
-
-theorem is_equivalence.is_symmetric [instance]
-        {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_symmetric R :=
-is_equivalence.rec (λx y z, y) C
-
-theorem is_equivalence.is_transitive [instance]
-       {T : Type} {R : T → T → Type} {C : is_equivalence R} : is_transitive R :=
-is_equivalence.rec (λx y z, z) C
+structure is_equivalence [class] {T : Type} (R : T → T → Type)
+extends is_reflexive R, is_symmetric R, is_transitive R
 
 -- partial equivalence relation
-inductive is_PER {T : Type} (R : T → T → Type) : Prop :=
-mk : is_symmetric R → is_transitive R → is_PER R
+structure is_PER {T : Type} (R : T → T → Type) extends is_symmetric R, is_transitive R
 
-theorem is_PER.is_symmetric [instance]
-        {T : Type} {R : T → T → Type} {C : is_PER R} : is_symmetric R :=
-is_PER.rec (λx y, x) C
+-- Generic notation. For example, is_refl R is the reflexivity of R, if that can be
+-- inferred by type class inference
+section
+  variables {T : Type} (R : T → T → Type)
+  definition rel_refl [C : is_reflexive R] := is_reflexive.refl R
+  definition rel_symm [C : is_symmetric R] := is_symmetric.symm R
+  definition rel_trans [C : is_transitive R] := is_transitive.trans R
+end
 
-theorem is_PER.is_transitive [instance]
-        {T : Type} {R : T → T → Type} {C : is_PER R} : is_transitive R :=
-  is_PER.rec (λx y, y) C
 
--- Congruence for unary and binary functions
--- -----------------------------------------
+/- classes for unary and binary congruences with respect to arbitrary relations -/
 
-inductive congruence [class] {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    (f : T1 → T2) : Prop :=
-mk : (∀x y, R1 x y → R2 (f x) (f y)) → congruence R1 R2 f
+structure is_congruence [class]
+  {T1 : Type} (R1 : T1 → T1 → Prop)
+  {T2 : Type} (R2 : T2 → T2 → Prop)
+  (f : T1 → T2) :=
+(congr : ∀{x y}, R1 x y → R2 (f x) (f y))
 
--- for binary functions
-inductive congruence2 [class] {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
-mk : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
-    congruence2 R1 R2 R3 f
+structure is_congruence2 [class]
+  {T1 : Type} (R1 : T1 → T1 → Prop)
+  {T2 : Type} (R2 : T2 → T2 → Prop)
+  {T3 : Type} (R3 : T3 → T3 → Prop)
+  (f : T1 → T2 → T3) :=
+(congr2 : ∀{x1 y1 : T1} {x2 y2 : T2}, R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2))
 
-namespace congruence
+namespace is_congruence
 
+  -- makes the type class explicit
   definition app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
-      {f : T1 → T2} (C : congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-  rec (λu, u) C x y
-
-  theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-      (f : T1 → T2) [C : congruence R1 R2 f] ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-  rec (λu, u) C x y
+      {f : T1 → T2} (C : is_congruence R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+  is_congruence.rec (λu, u) C x y
 
   definition app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
       {T3 : Type} {R3 : T3 → T3 → Prop}
-      {f : T1 → T2 → T3} (C : congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
+      {f : T1 → T2 → T3} (C : is_congruence2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄ :
     R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
-  congruence2.rec (λu, u) C x1 y1 x2 y2
+  is_congruence2.rec (λu, u) C x1 y1 x2 y2
 
--- ### general tools to build instances
+  /- tools to build instances -/
 
   theorem compose
       {T2 : Type} {R2 : T2 → T2 → Prop}
       {T3 : Type} {R3 : T3 → T3 → Prop}
-      {g : T2 → T3} (C2 : congruence R2 R3 g)
+      {g : T2 → T3} (C2 : is_congruence R2 R3 g)
       ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
-      {f : T1 → T2} (C1 : congruence R1 R2 f) :
-    congruence R1 R3 (λx, g (f x)) :=
-  mk (λx1 x2 H, app C2 (app C1 H))
+      {f : T1 → T2} (C1 : is_congruence R1 R2 f) :
+    is_congruence R1 R3 (λx, g (f x)) :=
+  is_congruence.mk (λx1 x2 H, app C2 (app C1 H))
 
   theorem compose21
       {T2 : Type} {R2 : T2 → T2 → Prop}
       {T3 : Type} {R3 : T3 → T3 → Prop}
       {T4 : Type} {R4 : T4 → T4 → Prop}
-      {g : T2 → T3 → T4} (C3 : congruence2 R2 R3 R4 g)
+      {g : T2 → T3 → T4} (C3 : is_congruence2 R2 R3 R4 g)
       ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
-      {f1 : T1 → T2} (C1 : congruence R1 R2 f1)
-      {f2 : T1 → T3} (C2 : congruence R1 R3 f2) :
-    congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
-  mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
+      {f1 : T1 → T2} (C1 : is_congruence R1 R2 f1)
+      {f2 : T1 → T3} (C2 : is_congruence R1 R3 f2) :
+    is_congruence R1 R4 (λx, g (f1 x) (f2 x)) :=
+  is_congruence.mk (λx1 x2 H, app2 C3 (app C1 H) (app C2 H))
 
   theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : relation.reflexive R2)
       ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
-    congruence R1 R2 (λu : T1, c) :=
-  mk (λx y H1, H c)
+    is_congruence R1 R2 (λu : T1, c) :=
+  is_congruence.mk (λx y H1, H c)
 
-end congruence
-
--- Notice these can't be in the congruence namespace, if we want it visible without
--- using congruence.
+end is_congruence
 
 theorem congruence_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
     [C : is_reflexive R2] ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
-  congruence R1 R2 (λu : T1, c) :=
-congruence.const R2 (is_reflexive.app C) R1 c
+  is_congruence R1 R2 (λu : T1, c) :=
+is_congruence.const R2 (is_reflexive.refl R2) R1 c
 
 theorem congruence_trivial [instance] {T : Type} (R : T → T → Prop) :
-  congruence R R (λu, u) :=
-congruence.mk (λx y H, H)
+  is_congruence R R (λu, u) :=
+is_congruence.mk (λx y H, H)
 
 
--- Relations that can be coerced to functions / implications
--- ---------------------------------------------------------
+/- relations that can be coerced to functions / implications-/
 
-inductive mp_like [class] {R : Type → Type → Prop} {a b : Type} (H : R a b) : Type :=
-mk {} : (a → b) → mp_like H
+structure mp_like [class] (R : Type → Type → Type) :=
+(app : Π{a b : Type}, R a b → (a → b))
 
-namespace mp_like
+definition rel_mp (R : Type → Type → Type) [C : mp_like R] {a b : Type} (H : R a b) :=
+mp_like.app H
 
-  definition app.{l} {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
-    (C : mp_like H) : a → b := rec (λx, x) C
-
-  definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
-    {C : mp_like H} : a → b := rec (λx, x) C
-
-end mp_like
-
-
--- Notation for operations on general symbols
--- ------------------------------------------
-
--- e.g. if R is an instance of the class, then "refl R" is reflexivity for the class
-definition rel_refl := is_reflexive.infer
-definition rel_symm := is_symmetric.infer
-definition rel_trans := is_transitive.infer
-definition rel_mp := mp_like.infer
 
 end relation
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index e6d489572..fa8670a42 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -47,10 +47,7 @@ have H3 : pr1 a + pr2 c + pr2 b = pr2 a + pr1 c + pr2 b, from
 show pr1 a + pr2 c = pr2 a + pr1 c, from add.cancel_right H3
 
 theorem rel_equiv : is_equivalence rel :=
-is_equivalence.mk
-  (is_reflexive.mk @rel_refl)
-  (is_symmetric.mk @rel_symm)
-  (is_transitive.mk @rel_trans)
+is_equivalence.mk @rel_refl @rel_symm @rel_trans
 
 theorem rel_flip {a b : ℕ × ℕ} (H : rel a b) : rel (flip a) (flip b) :=
 calc
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index d9f7d48db..ad0fefa80 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -21,14 +21,14 @@ definition prelim_map {A : Type} (R : A → A → Prop) (a : A) :=
 -- TODO: only needed R reflexive (or weaker: R a a)
 theorem prelim_map_rel {A : Type} {R : A → A → Prop} (H : is_equivalence R) (a : A)
   : R a (prelim_map R a) :=
-have reflR : reflexive R, from is_reflexive.infer R,
+have reflR : reflexive R, from is_equivalence.refl R,
 epsilon_spec (exists_intro a (reflR a))
 
 -- TODO: only needed: R PER
 theorem prelim_map_congr {A : Type} {R : A → A → Prop} (H1 : is_equivalence R) {a b : A}
   (H2 : R a b) : prelim_map R a = prelim_map R b :=
-have symmR : relation.symmetric R, from is_symmetric.infer R,
-have transR : relation.transitive R, from is_transitive.infer R,
+have symmR : relation.symmetric R, from is_equivalence.symm R,
+have transR : relation.transitive R, from is_equivalence.trans R,
 have H3 : ∀c, R a c ↔ R b c, from
   take c,
     iff.intro
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index 26a8b3f4a..b05db0d9d 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -1,9 +1,10 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- logic.axioms.classical
--- ======================
+Module: logic.axims.classical
+Author: Leonardo de Moura
+-/
 
 import logic.quantifiers logic.cast algebra.relation
 
@@ -49,8 +50,8 @@ propext
   (assume H, eq_to_iff H)
 
 open relation
-theorem iff_congruence [instance] (P : Prop → Prop) : congruence iff iff P :=
-congruence.mk
+theorem iff_congruence [instance] (P : Prop → Prop) : is_congruence iff iff P :=
+is_congruence.mk
   (take (a b : Prop),
     assume H : a ↔ b,
     show P a ↔ P b, from eq_to_iff (iff_to_eq H ▸ eq.refl (P a)))
diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean
index 54fdc674d..df8cf504f 100644
--- a/library/logic/examples/instances_test.lean
+++ b/library/logic/examples/instances_test.lean
@@ -1,47 +1,38 @@
---- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Jeremy Avigad
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: logic.examples.instances_test
+Author: Jeremy Avigad
+
+Illustrates substitution and congruence with iff.
+-/
 
 import ..instances
-
 open relation
-open relation.general_operations
+open relation.general_subst
 open relation.iff_ops
 open eq.ops
 
-section
+example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
 
-theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
-
-end
-
-
-section
-
-theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
+example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 subst iff H1 H2
 
-theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
+example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
 H1 ▸ H2
 
-end
+example (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
+is_congruence.congr iff (λa, (a ∨ c → ¬(d → a))) H1
 
-
-theorem test4 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
-congruence.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
-
-
-section
-
-theorem test5 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
+example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
 H1 ⬝ H2⁻¹ ⬝ H3
 
-theorem test6 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
+example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
 H1 ⬝ (H2⁻¹ ⬝ H3)
 
-theorem test7 (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
+example (T : Type) (a b c d : T) (H1 : a = b) (H2 : c = b) (H3 : c = d) : a = d :=
 H1 ⬝ H2⁻¹ ⬝ H3
 
-theorem test8 (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
+example (a b c d : Prop) (H1 : a ↔ b) (H2 : c ↔ b) (H3 : c ↔ d) : a ↔ d :=
 H1 ⬝ H2⁻¹ ⬝ H3
-end
diff --git a/library/logic/instances.lean b/library/logic/instances.lean
index a3eeedcea..44d1ebee7 100644
--- a/library/logic/instances.lean
+++ b/library/logic/instances.lean
@@ -1,126 +1,97 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Jeremy Avigad
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 
--- logic.instances
--- ====================
+Module: logic.instances
+Author: Jeremy Avigad
+
+Class instances for iff and eq.
+-/
 
 import logic.connectives algebra.relation
 
 namespace relation
 
-open relation
+/- logical equivalence relations -/
 
--- Congruences for logic
--- ---------------------
+theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
+relation.is_equivalence.mk (@eq.refl T) (@eq.symm T) (@eq.trans T)
 
-theorem congruence_not : congruence iff iff not :=
-congruence.mk
+theorem is_equivalence_iff [instance] : relation.is_equivalence iff :=
+relation.is_equivalence.mk @iff.refl @iff.symm @iff.trans
+
+
+/- congruences for logic operations -/
+
+theorem is_congruence_not : is_congruence iff iff not :=
+is_congruence.mk
   (take a b,
     assume H : a ↔ b, iff.intro
       (assume H1 : ¬a, assume H2 : b, H1 (iff.elim_right H H2))
       (assume H1 : ¬b, assume H2 : a, H1 (iff.elim_left H H2)))
 
-theorem congruence_and : congruence2 iff iff iff and :=
-congruence2.mk
+theorem is_congruence_and : is_congruence2 iff iff iff and :=
+is_congruence2.mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff.intro
       (assume H3 : a1 ∧ a2, and.imp_and H3 (iff.elim_left H1) (iff.elim_left H2))
       (assume H3 : b1 ∧ b2, and.imp_and H3 (iff.elim_right H1) (iff.elim_right H2)))
 
-theorem congruence_or : congruence2 iff iff iff or :=
-congruence2.mk
+theorem is_congruence_or : is_congruence2 iff iff iff or :=
+is_congruence2.mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff.intro
       (assume H3 : a1 ∨ a2, or.imp_or H3 (iff.elim_left H1) (iff.elim_left H2))
       (assume H3 : b1 ∨ b2, or.imp_or H3 (iff.elim_right H1) (iff.elim_right H2)))
 
-theorem congruence_imp : congruence2 iff iff iff imp :=
-congruence2.mk
+theorem is_congruence_imp : is_congruence2 iff iff iff imp :=
+is_congruence2.mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff.intro
       (assume H3 : a1 → a2, assume Hb1 : b1, iff.elim_left H2 (H3 ((iff.elim_right H1) Hb1)))
       (assume H3 : b1 → b2, assume Ha1 : a1, iff.elim_right H2 (H3 ((iff.elim_left H1) Ha1))))
 
-theorem congruence_iff : congruence2 iff iff iff iff :=
-congruence2.mk
+theorem is_congruence_iff : is_congruence2 iff iff iff iff :=
+is_congruence2.mk
   (take a1 b1 a2 b2,
     assume H1 : a1 ↔ b1, assume H2 : a2 ↔ b2,
     iff.intro
       (assume H3 : a1 ↔ a2, iff.trans (iff.symm H1) (iff.trans H3 H2))
       (assume H3 : b1 ↔ b2, iff.trans H1 (iff.trans H3 (iff.symm H2))))
 
--- theorem congruence_const_iff [instance] := congruence.const iff iff.refl
-definition congruence_not_compose [instance] := congruence.compose congruence_not
-definition congruence_and_compose [instance] := congruence.compose21 congruence_and
-definition congruence_or_compose [instance] := congruence.compose21 congruence_or
-definition congruence_implies_compose [instance] := congruence.compose21 congruence_imp
-definition congruence_iff_compose [instance] := congruence.compose21 congruence_iff
-
--- Generalized substitution
--- ------------------------
-
--- TODO: note that the target has to be "iff". Otherwise, there is not enough
--- information to infer an mp-like relation.
-
-namespace general_operations
-
-theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : congruence R iff P]
-  {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (congruence.app C H) H1
-
-end general_operations
-
--- = is an equivalence relation
--- ----------------------------
-
-theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive (@eq T) :=
-relation.is_reflexive.mk (@eq.refl T)
-
-theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric (@eq T) :=
-relation.is_symmetric.mk (@eq.symm T)
-
-theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive (@eq T) :=
-relation.is_transitive.mk (@eq.trans T)
-
--- TODO: this is only temporary, needed to inform Lean that is_equivalence is a class
-theorem is_equivalence_eq [instance] (T : Type) : relation.is_equivalence (@eq T) :=
-relation.is_equivalence.mk _ _ _
+-- theorem is_congruence_const_iff [instance] := is_congruence.const iff iff.refl
+definition is_congruence_not_compose [instance] := is_congruence.compose is_congruence_not
+definition is_congruence_and_compose [instance] := is_congruence.compose21 is_congruence_and
+definition is_congruence_or_compose [instance] := is_congruence.compose21 is_congruence_or
+definition is_congruence_implies_compose [instance] := is_congruence.compose21 is_congruence_imp
+definition is_congruence_iff_compose [instance] := is_congruence.compose21 is_congruence_iff
 
 
--- iff is an equivalence relation
--- ------------------------------
+/- a general substitution operation with respect to an arbitrary congruence -/
 
-theorem is_reflexive_iff [instance] : relation.is_reflexive iff :=
-relation.is_reflexive.mk (@iff.refl)
-
-theorem is_symmetric_iff [instance] : relation.is_symmetric iff :=
-relation.is_symmetric.mk (@iff.symm)
-
-theorem is_transitive_iff [instance] : relation.is_transitive iff :=
-relation.is_transitive.mk (@iff.trans)
+namespace general_subst
+  theorem subst {T : Type} (R : T → T → Prop) ⦃P : T → Prop⦄ [C : is_congruence R iff P]
+    {a b : T} (H : R a b) (H1 : P a) : P b := iff.elim_left (is_congruence.app C H) H1
+end general_subst
 
 
--- Mp-like for iff
--- ---------------
+/- iff can be coerced to implication -/
 
-theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : @relation.mp_like iff a b H :=
-relation.mp_like.mk (iff.elim_left H)
+definition mp_like_iff [instance] : relation.mp_like iff :=
+relation.mp_like.mk (λa b (H : a ↔ b), iff.elim_left H)
 
 
--- Substition for iff
--- ------------------
+/- support for calculations with iff -/
+
 namespace iff
-theorem subst {P : Prop → Prop} [C : congruence iff iff P] {a b : Prop} (H : a ↔ b) (H1 : P a) :
-  P b :=
-@general_operations.subst Prop iff P C a b H H1
+  theorem subst {P : Prop → Prop} [C : is_congruence iff iff P] {a b : Prop} (H : a ↔ b) (H1 : P a) :
+    P b :=
+  @general_subst.subst Prop iff P C a b H H1
 end iff
 
--- Support for calculations with iff
--- ----------------
-
 calc_subst iff.subst
 
 namespace iff_ops
@@ -133,4 +104,5 @@ namespace iff_ops
   definition subst := @iff.subst
   definition mp    := @iff.mp
 end iff_ops
+
 end relation