move wf_nat_ind to a common place

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.

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 :=

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.