diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean
index 7a4566f14..ed72043ac 100644
--- a/library/standard/data/list/basic.lean
+++ b/library/standard/data/list/basic.lean
@@ -15,7 +15,6 @@ import logic
 -- import if -- for find
 
 using nat
-using congr
 using eq_proofs
 
 namespace list
@@ -289,4 +288,4 @@ end
 -- declare global notation outside the section
 infixl `++` : 65 := concat
 
-end list
\ No newline at end of file
+end list
diff --git a/library/standard/logic/axioms/funext.lean b/library/standard/logic/axioms/funext.lean
index f92f77557..79ce0419d 100644
--- a/library/standard/logic/axioms/funext.lean
+++ b/library/standard/logic/axioms/funext.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.connectives.eq logic.connectives.function
+import logic.connectives.eq struc.function
 using function
 
 -- Function extensionality
@@ -25,4 +25,4 @@ section
   theorem compose_const_right (f : B → C) (b : B) : f ∘ (const A b) = const A (f b) :=
   funext (take x, refl _)
 end
-end function
\ No newline at end of file
+end function
diff --git a/library/standard/logic/classes/congr.lean b/library/standard/logic/classes/congr.lean
deleted file mode 100644
index 00303fdaf..000000000
--- a/library/standard/logic/classes/congr.lean
+++ /dev/null
@@ -1,140 +0,0 @@
-----------------------------------------------------------------------------------------------------
---- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
---- Released under Apache 2.0 license as described in the file LICENSE.
---- Author: Jeremy Avigad
-----------------------------------------------------------------------------------------------------
-
-import logic.connectives.basic logic.connectives.function
-using function
-namespace congr
-
--- TODO: move this somewhere else
-abbreviation reflexive {T : Type} (R : T → T → Type) : Prop := ∀x, R x x
-
-
--- Congruence classes for unary and binary functions
--- -------------------------------------------------
-
-inductive class {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    (f : T1 → T2) : Prop :=
-| mk : (∀x y : T1, R1 x y → R2 (f x) (f y)) → class R1 R2 f
-
-abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
-    {f : T1 → T2} (C : class R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-class_rec id C x y
-
--- to trigger class inference
-theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    (f : T1 → T2) {C : class R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
-class_rec id C x y
-
--- for binary functions
-inductive class2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
-    {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
-| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
-    class2 R1 R2 R3 f
-
-abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
-    {T3 : Type} {R3 : T3 → T3 → Prop}
-    {f : T1 → T2 → T3} (C : class2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄
-  : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
-class2_rec id C x1 y1 x2 y2
-
-
--- General tools to build instances
--- --------------------------------
-
-theorem compose
-    {T2 : Type} {R2 : T2 → T2 → Prop}
-    {T3 : Type} {R3 : T3 → T3 → Prop}
-    {g : T2 → T3} (C2 : congr.class R2 R3 g)
-    {{T1 : Type}} {R1 : T1 → T1 → Prop}
-    {f : T1 → T2} (C1 : congr.class R1 R2 f) :
-  congr.class R1 R3 (λx, g (f x)) := mk (take 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 : congr.class2 R2 R3 R4 g)
-    ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
-    {f1 : T1 → T2} (C1 : congr.class R1 R2 f1)
-    {f2 : T1 → T3} (C2 : congr.class R1 R3 f2) :
-  congr.class R1 R4 (λx, g (f1 x) (f2 x)) := mk (take x1 x2 H, app2 C3 (app C1 H) (app C2 H))
-
-theorem trivial [instance] {T : Type} (R : T → T → Prop) : class R R id :=
-mk (take x y H, H)
-
-theorem const {T2 : Type} (R2 : T2 → T2 → Prop) (H : reflexive R2) :
-  ∀(T1 : Type) (R1 : T1 → T1 → Prop) (c : T2), class R1 R2 (function.const T1 c) :=
-take T1 R1 c, mk (take x y H1, H c)
-
-
--- instances for logic
--- -------------------
-
-theorem congr_not : congr.class iff iff not :=
-congr.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 congr_and : congr.class2 iff iff iff and :=
-congr.mk2
-  (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 congr_or : congr.class2 iff iff iff or :=
-congr.mk2
-  (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 congr_imp : congr.class2 iff iff iff imp :=
-congr.mk2
-  (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 congr_iff : congr.class2 iff iff iff iff :=
-congr.mk2
-  (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 congr_const_iff [instance] := congr.const iff iff_refl
-theorem congr_not_compose [instance] := congr.compose congr_not
-theorem congr_and_compose [instance] := congr.compose21 congr_and
-theorem congr_or_compose [instance] := congr.compose21 congr_or
-theorem congr_implies_compose [instance] := congr.compose21 congr_imp
-theorem congr_iff_compose [instance] := congr.compose21 congr_iff
-
-theorem subst_iff {T : Type} {R : T → T → Prop} {P : T → Prop} {C : class R iff P}
-  {a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (app C H) H1
-
-theorem test1 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
-congr.infer iff iff _ H1
-
-theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
-subst_iff H1 H2
-
--- TODO: move these to new file
-
-theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
-calc
-  (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
-    ... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c)
-    ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
-
--- TODO: add or_left_comm, and_right_comm, and_left_comm
-end congr
\ No newline at end of file
diff --git a/library/standard/logic/connectives/connectives.md b/library/standard/logic/connectives/connectives.md
index d547aebd3..e5789280b 100644
--- a/library/standard/logic/connectives/connectives.md
+++ b/library/standard/logic/connectives/connectives.md
@@ -4,9 +4,9 @@ logic.connectives
 Logical operations and connectives.
 
 * [prop](prop.lean) : the type Prop
-* [function](function.lean) : notation for functions
 * [basic](basic.lean) : propositional connectives
 * [eq](eq.lean) : equality and disequality
 * [cast](cast.lean) : casts and heterogeneous equality
 * [quantifiers](quantifiers.lean) : existential and universal quantifiers
 * [if](if.lean) : if-then-else
+* [instances](instances.lean) : type class instances
\ No newline at end of file
diff --git a/library/standard/logic/connectives/instances.lean b/library/standard/logic/connectives/instances.lean
new file mode 100644
index 000000000..044afccf1
--- /dev/null
+++ b/library/standard/logic/connectives/instances.lean
@@ -0,0 +1,167 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.basic logic.connectives.eq struc.relation
+
+using relation
+
+-- Congruences for logic
+-- ---------------------
+
+theorem congr_not : congr.class iff iff not :=
+congr.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 congr_and : congr.class2 iff iff iff and :=
+congr.mk2
+  (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 congr_or : congr.class2 iff iff iff or :=
+congr.mk2
+  (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 congr_imp : congr.class2 iff iff iff imp :=
+congr.mk2
+  (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 congr_iff : congr.class2 iff iff iff iff :=
+congr.mk2
+  (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 congr_const_iff [instance] := congr.const iff iff_refl
+theorem congr_not_compose [instance] := congr.compose congr_not
+theorem congr_and_compose [instance] := congr.compose21 congr_and
+theorem congr_or_compose [instance] := congr.compose21 congr_or
+theorem congr_implies_compose [instance] := congr.compose21 congr_imp
+theorem congr_iff_compose [instance] := congr.compose21 congr_iff
+
+
+-- Generalized substitution
+-- ------------------------
+
+namespace gensubst
+
+-- TODO: note that the target has to be "iff". Otherwise, there is not enough
+-- information to infer an mp-like relation.
+
+theorem subst {T : Type} {R : T → T → Prop} {P : T → Prop} {C : congr.class R iff P}
+  {a b : T} (H : R a b) (H1 : P a) : P b := iff_elim_left (congr.app C H) H1
+
+infixr `▸`:75    := subst
+
+end -- gensubst
+
+
+-- = is an equivalence relation
+-- ----------------------------
+
+theorem is_reflexive_eq [instance] (T : Type) : relation.is_reflexive.class (@eq T) :=
+relation.is_reflexive.mk (@refl T)
+
+theorem is_symmetric_eq [instance] (T : Type) : relation.is_symmetric.class (@eq T) :=
+relation.is_symmetric.mk (@symm T)
+
+theorem is_transitive_eq [instance] (T : Type) : relation.is_transitive.class (@eq T) :=
+relation.is_transitive.mk (@trans T)
+
+
+-- iff is an equivalence relation
+-- ------------------------------
+
+theorem is_reflexive_iff [instance] : relation.is_reflexive.class iff :=
+relation.is_reflexive.mk (@iff_refl)
+
+theorem is_symmetric_iff [instance] : relation.is_symmetric.class iff :=
+relation.is_symmetric.mk (@iff_symm)
+
+theorem is_transitive_iff [instance] : relation.is_transitive.class iff :=
+relation.is_transitive.mk (@iff_trans)
+
+
+-- Mp-like for iff
+-- ---------------
+
+theorem mp_like_iff [instance] (a b : Prop) (H : a ↔ b) : relation.mp_like.class H :=
+relation.mp_like.mk (iff_elim_left H)
+
+
+-- Tests
+-- -----
+
+namespace logic_instances_tests
+
+section
+
+using relation.operations
+
+theorem test1 (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
+
+end
+
+
+section
+
+using gensubst
+
+theorem test2 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
+subst H1 H2
+
+theorem test3 (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
+H1 ▸ H2
+
+end
+
+theorem test4 (a b c d e : Prop) (H1 : a ↔ b) : (a ∨ c → ¬(d → a)) ↔ (b ∨ c → ¬(d → b)) :=
+congr.infer iff iff (λa, (a ∨ c → ¬(d → a))) H1
+
+
+section
+
+using relation.symbols
+
+theorem test5 (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 :=
+H1 ⬝ (H2⁻¹ ⬝ H3)
+
+end
+
+end
+
+
+-- Boolean calculations
+-- --------------------
+
+-- TODO: move these to new file
+-- TODO: declare trans
+
+theorem or_right_comm (a b c : Prop) : (a ∨ b) ∨ c ↔ (a ∨ c) ∨ b :=
+calc
+  (a ∨ b) ∨ c ↔ a ∨ (b ∨ c) : or_assoc _ _ _
+    ... ↔ a ∨ (c ∨ b) : congr.infer iff iff _ (or_comm b c)
+    ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _)
+
+-- TODO: add or_left_comm, and_right_comm, and_left_comm
diff --git a/library/standard/logic/default.lean b/library/standard/logic/default.lean
index 302573209..e83054bbd 100644
--- a/library/standard/logic/default.lean
+++ b/library/standard/logic/default.lean
@@ -5,5 +5,5 @@
 ----------------------------------------------------------------------------------------------------
 
 import logic.connectives.basic logic.connectives.eq logic.connectives.quantifiers
-import logic.classes.decidable logic.classes.inhabited logic.classes.congr
+import logic.classes.decidable logic.classes.inhabited logic.connectives.instances
 import logic.connectives.if
\ No newline at end of file
diff --git a/library/standard/logic/connectives/function.lean b/library/standard/struc/function.lean
similarity index 100%
rename from library/standard/logic/connectives/function.lean
rename to library/standard/struc/function.lean
diff --git a/library/standard/struc/relation.lean b/library/standard/struc/relation.lean
new file mode 100644
index 000000000..7abb043ba
--- /dev/null
+++ b/library/standard/struc/relation.lean
@@ -0,0 +1,172 @@
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic.connectives.prop
+
+-- General properties of relations
+-- -------------------------------
+
+namespace relation
+
+abbreviation reflexive {T : Type} (R : T → T → Type) : Type := ∀x, R x x
+abbreviation symmetric {T : Type} (R : T → T → Type) : Type := ∀x y, R x y → R y x
+abbreviation transitive {T : Type} (R : T → T → Type) : Type := ∀x y z, R x y → R y z → R x z
+
+namespace is_reflexive
+
+inductive class {T : Type} (R : T → T → Type)  : Prop :=
+| mk : reflexive R → class R
+
+abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) : reflexive R
+:= class_rec (λu, u) C
+
+abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} : reflexive R
+:= class_rec (λu, u) C
+
+end -- is_reflexive
+
+namespace is_symmetric
+
+inductive class {T : Type} (R : T → T → Type)  : Prop :=
+| mk : symmetric R → class R
+
+abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y : T⦄ (H : R x y) : R y x
+:= class_rec (λu, u) C x y H
+
+abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y : T⦄ (H : R x y) : R y x
+:= class_rec (λu, u) C x y H
+
+end -- is_symmetric
+
+namespace is_transitive
+
+inductive class {T : Type} (R : T → T → Type)  : Prop :=
+| mk : transitive R → class R
+
+abbreviation app ⦃T : Type⦄ {R : T → T → Type} (C : class R) ⦃x y z : T⦄ (H1 : R x y)
+  (H2 : R y z) : R x z
+:= class_rec (λu, u) C x y z H1 H2
+
+abbreviation infer ⦃T : Type⦄ {R : T → T → Type} {C : class R} ⦃x y z : T⦄ (H1 : R x y)
+  (H2 : R y z) : R x z
+:= class_rec (λu, u) C x y z H1 H2
+
+end -- is_transitive
+
+
+-- Congruence for unary and binary functions
+-- -----------------------------------------
+
+namespace congr
+
+inductive 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)) → class R1 R2 f
+
+abbreviation app {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
+    {f : T1 → T2} (C : class R1 R2 f) ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+class_rec (λu, u) C x y
+
+theorem infer {T1 : Type} (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+    (f : T1 → T2) {C : class R1 R2 f} ⦃x y : T1⦄ : R1 x y → R2 (f x) (f y) :=
+class_rec (λu, u) C x y
+
+-- for binary functions
+inductive class2 {T1 : Type}  (R1 : T1 → T1 → Prop) {T2 : Type} (R2 : T2 → T2 → Prop)
+    {T3 : Type} (R3 : T3 → T3 → Prop) (f : T1 → T2 → T3) : Prop :=
+| mk2 : (∀(x1 y1 : T1) (x2 y2 : T2), R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2)) →
+    class2 R1 R2 R3 f
+
+abbreviation app2 {T1 : Type} {R1 : T1 → T1 → Prop} {T2 : Type} {R2 : T2 → T2 → Prop}
+    {T3 : Type} {R3 : T3 → T3 → Prop}
+    {f : T1 → T2 → T3} (C : class2 R1 R2 R3 f) ⦃x1 y1 : T1⦄ ⦃x2 y2 : T2⦄
+  : R1 x1 y1 → R2 x2 y2 → R3 (f x1 x2) (f y1 y2) :=
+class2_rec (λu, u) C x1 y1 x2 y2
+
+-- ### general tools to build instances
+
+theorem compose
+    {T2 : Type} {R2 : T2 → T2 → Prop}
+    {T3 : Type} {R3 : T3 → T3 → Prop}
+    {g : T2 → T3} (C2 : congr.class R2 R3 g)
+    {{T1 : Type}} {R1 : T1 → T1 → Prop}
+    {f : T1 → T2} (C1 : congr.class R1 R2 f) :
+  congr.class R1 R3 (λx, g (f x)) :=
+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 : congr.class2 R2 R3 R4 g)
+    ⦃T1 : Type⦄ {R1 : T1 → T1 → Prop}
+    {f1 : T1 → T2} (C1 : congr.class R1 R2 f1)
+    {f2 : T1 → T3} (C2 : congr.class R1 R3 f2) :
+  congr.class R1 R4 (λx, g (f1 x) (f2 x)) :=
+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) :
+  class R1 R2 (λu : T1, c) :=
+mk (λx y H1, H c)
+
+end -- namespace congr
+
+end -- namespace relation
+
+
+-- TODO: notice these can't be in the congr namespace, if we want it visible without
+-- using congr.
+
+theorem congr_const [instance] {T2 : Type} (R2 : T2 → T2 → Prop)
+    {C : relation.is_reflexive.class R2} ⦃T1 : Type⦄ (R1 : T1 → T1 → Prop) (c : T2) :
+  relation.congr.class R1 R2 (λu : T1, c) :=
+relation.congr.const R2 (relation.is_reflexive.app C) R1 c
+
+theorem congr_trivial [instance] {T : Type} (R : T → T → Prop) :
+  relation.congr.class R R (λu, u) :=
+relation.congr.mk (λx y H, H)
+
+
+-- Relations that can be coerced to functions / implications
+-- ---------------------------------------------------------
+
+namespace relation
+
+namespace mp_like
+
+inductive class {R : Type → Type → Prop} {a b : Type} (H : R a b) : Prop :=
+| mk {} : (a → b) → @class R a b H
+
+definition app {R : Type → Type → Prop} {a : Type} {b : Type} {H : R a b}
+  (C : class H) : a → b := class_rec (λx, x) C
+
+definition infer ⦃R : Type → Type → Prop⦄ {a : Type} {b : Type} (H : R a b)
+  {C : class H} : a → b := class_rec (λx, x) C
+
+end -- namespace mp_like
+
+
+-- Notation for operations on general symbols
+-- ------------------------------------------
+
+namespace operations
+
+definition refl := is_reflexive.infer
+definition symm := is_symmetric.infer
+definition trans := is_transitive.infer
+definition mp := mp_like.infer
+
+end -- namespace operations
+
+namespace symbols
+
+postfix `⁻¹`:100 := operations.symm
+infixr `⬝`:75     := operations.trans
+
+end -- namespace symbols
+
+end -- namespace relation
diff --git a/library/standard/struc/struc.md b/library/standard/struc/struc.md
index 694c37dde..a100096df 100644
--- a/library/standard/struc/struc.md
+++ b/library/standard/struc/struc.md
@@ -3,6 +3,8 @@ struc
 
 Axiomatic properties and structures.
 
+* [function](function.lean)
+* [relation](relation.lean)
 * [binary](binary.lean) : binary operations
 * [equivalence](equivalence.lean) : equivalence relations
 * [wf](wf.lean) : well-founded relations