diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index bb428f74e..6ed67a359 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -273,7 +273,5 @@ namespace equiv
   attribute equiv.trans [trans]
   attribute equiv.refl [refl]
   attribute equiv.symm [symm]
-  attribute equiv_of_equiv_of_eq [trans]
-  attribute equiv_of_eq_of_equiv [trans]
 
 end equiv
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 984b503ff..f04050a50 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -125,9 +125,6 @@ section
   assume H₁ H₂, H₂ ▸ H₁
 end
 
-attribute ne.of_eq_of_ne [trans]
-attribute ne.of_ne_of_eq [trans]
-
 /- iff -/
 
 definition iff (a b : Type) := prod (a → b) (b → a)