diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 377e821b8..a9ce529ce 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -61,6 +61,9 @@ namespace eq
   end ops
 end eq
 
+theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
+eq.subst H₁ (eq.subst H₂ rfl)
+
 section
   variables {A : Type} {a b c: A}
   open eq.ops
diff --git a/library/init/logic.lean b/library/init/logic.lean
index f9b7cba8d..6da90b0ad 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -57,6 +57,9 @@ namespace eq
   end ops
 end eq
 
+theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂ :=
+eq.subst H₁ (eq.subst H₂ rfl)
+
 section
   variables {A : Type} {a b c: A}
   open eq.ops
diff --git a/library/logic/eq.lean b/library/logic/eq.lean
index 12db9e237..6a00db451 100644
--- a/library/logic/eq.lean
+++ b/library/logic/eq.lean
@@ -58,9 +58,6 @@ section
   theorem congr_arg (f : A → B) (H : a = a') : f a = f a' :=
   H ▸ rfl
 
-  theorem congr {f g : A → B} (H₁ : f = g) (H₂ : a = a') : f a = g a' :=
-  H₁ ▸ H₂ ▸ rfl
-
   theorem congr_arg2 (f : A → B → C) (Ha : a = a') (Hb : b = b') : f a b = f a' b' :=
   congr (congr_arg f Ha) Hb