iInduction does not work well for induction principles involving `Forall`

Simuliris has an interesting IntoIH instance to support doing iInduction ... using expr_ind, where expr_ind is a custom induction principle that uses Forall to handle nested lists.

Here's a self-contained testcase:

Inductive tree (T : Type) := Tree : list (tree T) → tree T.
Arguments Tree {T}.

Lemma tree_ind' T (P : tree T → Prop) :
  (∀ l, Forall P l → P (Tree l)) →
  ∀ t, P t.
Proof.
  intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
  induction l as [|t l IH].
  { constructor. }
  constructor; last apply IH.
  apply REC.
Qed.

Lemma test_iInduction_Forall (t : tree nat) (P : PROP) : ⊢ P.
Proof. iInduction t as [] "IH" using tree_ind'.

This shows a goal

 PROP : bi
  l : list (tree nat)
  P : PROP
  ============================
  "IH" : <pers> ?P
  --------------------------------------□
  P

An unshelve shows that the IntoIH simply was not resolved, which seems like a bug in its own right -- iInduction should fail in that case.

In fact this testcase is interesting in the sense that even adding the instance from Simuliris (even after getting rid of the BiAffine assumption) does not help:

Section tactics.
Import iris.bi.bi.
Import iris.proofmode.base environments classes modality_instances.
Import bi.
Import env_notations.
Context {PROP : bi}.
Implicit Types Γ : env PROP.
Implicit Types Δ : envs PROP.
Implicit Types P Q : PROP.

  Import coq_tactics.
  Local Instance into_ih_Forall {A} (φ : A → Prop) (l : list A) Δ Φ :
  (∀ x, x ∈ l → IntoIH (φ x) Δ (Φ x)) → IntoIH (Forall φ l) Δ (∀ x, ⌜x ∈ l⌝ → Φ x) | 2.
  Proof.
    rewrite /IntoIH Forall_forall => HΔ Hf. apply forall_intro=> x.
    iIntros "Henv %Hl".  iApply (HΔ with "Henv"); eauto.
  Qed.
End tactics.