# 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.
```