diff --git a/theories/relations.v b/theories/relations.v
index 5019e3f8876c448f0a8b65d39a54f39365955580..f6093bc93b341b83b5c05509d4b65c8e283441c3 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -1,7 +1,6 @@
 (** This file collects definitions and theorems on abstract rewriting systems.
 These are particularly useful as we define the operational semantics as a
 small step semantics. *)
-From Coq Require Import Wf_nat.
 From stdpp Require Export sets.
 From stdpp Require Import options.