diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index e271c84ddec5a4bb5344a70fc1d1fe6d460047ee..408ca28444abd5f058f03e9d69416357a53681d4 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -541,6 +541,16 @@ Proof.
   intros HΔ. by rewrite envs_clear_spatial_sound HΔ env_fold_wand wand_elim_l.
 Qed.
 
+Lemma tac_revert_ih Δ P Q :
+  env_spatial_is_nil Δ = true →
+  (of_envs Δ ⊢ P) →
+  (of_envs Δ ⊢ □ P → Q) →
+  (of_envs Δ ⊢ Q).
+Proof.
+  intros ? HP HPQ.
+  by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
+Qed.
+
 Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
   IntoAssert P Q R →
   envs_split lr js Δ = Some (Δ1,Δ2) →
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index c06a27dbf05b625f6cd74ef1aac1adc1fbdbe6b3..3411a43617d92fdaa48ef6e3ad635bbcd09bb32c 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -877,12 +877,31 @@ Tactic Notation "iDestruct" open_constr(lem) "as" "(" simple_intropattern(x1)
 Tactic Notation "iDestruct" open_constr(lem) "as" "%" simple_intropattern(pat) :=
   iDestructCore lem as true (fun H => iPure H as pat).
 
+(** * Induction *)
+Tactic Notation "iInductionCore" constr(x)
+    "as" simple_intropattern(pat) constr(IH) :=
+  let rec fix_ihs :=
+    lazymatch goal with
+    | H : coq_tactics.of_envs _ ⊢ _ |- _ =>
+       eapply tac_revert_ih;
+         [env_cbv; reflexivity
+         |apply H|];
+       clear H; fix_ihs;
+       let IH' := iFresh' IH in iIntros [IAlwaysElim (IName IH')]
+    | _ => idtac
+    end in
+  induction x as pat; fix_ihs.
+
+Tactic Notation "iInduction" constr(x)
+    "as" simple_intropattern(pat) constr(IH) :=
+  iRevertIntros with (iInductionCore x as pat IH).
+
+(** * Löb Induction *)
 Tactic Notation "iLöbCore" "as" constr (IH) :=
   eapply tac_löb with _ IH;
     [reflexivity
     |env_cbv; reflexivity || fail "iLöb:" IH "not fresh"|].
 
-(** * Löb induction *)
 Tactic Notation "iLöb" "as" constr (IH) :=
   iRevertIntros with (iLöbCore as IH).
 Tactic Notation "iLöb" "(" ident(x1) ")" "as" constr (IH) :=