diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index e174741cc34f1299f695098bb4c91f67a91663da..7986d8b3b6b759c01488ddc1da3ebc0c5c58118d 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -1769,9 +1769,9 @@ Ltac _iInduction x xs Hs tac IH :=
   (* FIXME: We should be able to do this in a more sane way, by concatenating
   the spec patterns instead of calling [iRevertIntros] multiple times. *)
   _iRevertIntros0 Hs ltac:(fun _ =>
-    _iRevertIntros xs "∗" ltac:(fun _ =>
+    _iRevertIntros0 "∗" ltac:(fun _ =>
       let Hsx := iHypsContaining x in
-      _iRevertIntros0 Hsx ltac:(fun _ =>
+      _iRevertIntros xs Hsx ltac:(fun _ =>
         iInductionCore tac as IH
       )
     )
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 578a2202fa672a8426f86ae2bcfac1bd12bd3b0f..31c0c4168b4909f54d37b0a936f0141bbfaa54e8 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -903,6 +903,17 @@ Proof.
     by iApply "IH".
 Qed.
 
+(* From https://gitlab.mpi-sws.org/iris/iris/-/issues/534 *)
+Lemma test_iInduction_big_sepL_impl' {A} (Φ Ψ : nat → A → PROP) (l1 l2 : list A) :
+  length l1 = length l2 →
+  ([∗ list] k↦x ∈ l1, Φ k x) -∗
+  □ (∀ k x1 x2, ⌜l1 !! k = Some x1⌝ -∗ ⌜l2 !! k = Some x2⌝ -∗ Φ k x1 -∗ Ψ k x2) -∗
+  [∗ list] k↦x ∈ l2, Ψ k x.
+Proof.
+  iIntros (Hlen) "Hl #Himpl".
+  iInduction l1 as [|x1 l1] "IH" forall (Φ Ψ l2 Hlen).
+Abort.
+
 Inductive tree := leaf | node (l r: tree).
 
 Check "test_iInduction_multiple_IHs".