`iInduction ... forall (xs)` does not revert persistent hypotheses containing `xs`
From iris.algebra Require Export big_op.
From iris.bi Require Import bi.
From iris.proofmode Require Import proofmode.
Lemma big_sepL_impl' {PROP : bi} {A B} (l1 : list A) (l2 : list B) :
⊢@{PROP} □ (∀ k x2, ⌜l2 !! k = Some x2⌝ -∗ True) -∗
True.
Proof. iIntros "#Himpl". iInduction l1 as [|x1 l1] "IH" forall (l2).
Example taken from #534 (closed)