diff --git a/library/init/funext.lean b/library/init/funext.lean
index 099b0cec7..acef03bf4 100644
--- a/library/init/funext.lean
+++ b/library/init/funext.lean
@@ -27,7 +27,7 @@ section
   λH₁ H₂ x, eq.trans (H₁ x) (H₂ x)
 
   private theorem fun_eqv.is_equivalence (A : Type) (B : A → Type) : equivalence (@fun_eqv A B) :=
-  and.intro (@fun_eqv.refl A B) (and.intro (@fun_eqv.symm A B) (@fun_eqv.trans A B))
+  mk_equivalence (@fun_eqv A B) (@fun_eqv.refl A B) (@fun_eqv.symm A B) (@fun_eqv.trans A B)
 
   definition fun_setoid [instance] (A : Type) (B : A → Type) : setoid (Πx : A, B x) :=
   setoid.mk (@fun_eqv A B) (fun_eqv.is_equivalence A B)
diff --git a/library/init/relation.lean b/library/init/relation.lean
index fbd3d83f5..672e4d0f0 100644
--- a/library/init/relation.lean
+++ b/library/init/relation.lean
@@ -22,6 +22,9 @@ definition transitive := ∀⦃x y z⦄, x ≺ y → y ≺ z → x ≺ z
 
 definition equivalence := reflexive R ∧ symmetric R ∧ transitive R
 
+definition mk_equivalence (r : reflexive R) (s : symmetric R) (t : transitive R) : equivalence R :=
+and.intro r (and.intro s t)
+
 definition irreflexive := ∀x, ¬ x ≺ x
 
 definition anti_symmetric := ∀⦃x y⦄, x ≺ y → y ≺ x → x = y