diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 203e9d70c28962e72e3c60e4bdbd0bb38d93a131..7bf2468e86c2864a5d35f3c815e5ce0a1b8009f1 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -56,8 +56,6 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
         rewrite EQv; reflexivity.
     Qed.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Lemma htBind P Q R K e safe m :
       ht safe m P e Q ∧ all (plugV safe m Q R K) ⊑ ht safe m P (K [[ e ]]) R.
     Proof.
diff --git a/iris_meta.v b/iris_meta.v
index 5f65742ad9913c595981c5b0d2ce1caa1807930e..d4382e3c79be2bc44a978a1ed4013c12f3261f41 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -200,8 +200,6 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
   Set Bullet Behavior "None".	(* PDS: Ridiculous. *)
   Section RobustSafety.
 
-    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
     Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state).
 
     Program Definition restrictV (Q : expr -n> Props) : vPred :=
diff --git a/iris_plog.v b/iris_plog.v
index 3df7d55d8804d273e73a536cb1c1aec6c3202595..7e8b99b433f7dc8927d2f401f8147bbddb31cc13 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -442,6 +442,9 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
 
     Definition ht safe m P e Q := □(P → wp safe m e Q).
 
+    (* People will need that *)
+    Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
+
   End HoareTriples.
 
 End IRIS_PLOG.