diff --git a/iris_plog.v b/iris_plog.v
index 6cac9c75161e76a72a9909150c13f0d0484b60f5..553ba9c5f35c81ffd1b3fed0e97e52910af5dab8 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -471,9 +471,6 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
   End HoareTriples.
 
-  (* Simple things, needed elsewhere. *)
-  Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
 End IRIS_PLOG.
 
 Module IrisPlog (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_PROP R) (CORE: IRIS_CORE RL C R WP) : IRIS_PLOG RL C R WP CORE.