diff --git a/CHANGELOG.md b/CHANGELOG.md
index 55208174eb36c1f0cf309b13c4042bc2e75c9b14..a6dd68403770af80409ca5048d4e468df58d0f22 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,8 @@ lemma.
    to occur when the conclusion contains variables that are not in scope of the
    evar, thus blocking the default behavior of instantiating the premise with
    the conclusion. The old behavior can be emulated with`iExFalso. iExact "H".`
+* `iInduction` now supports induction schemes that involve `Forall` and
+  `Forall2` (for example, for trees with finite branching).
 
 ## Iris 3.6.0 (2022-01-22)
 
diff --git a/iris/proofmode/coq_tactics.v b/iris/proofmode/coq_tactics.v
index 3e8effac70f102a26d69dc90bf4f8e048d7aeb0d..a2708b041d45ae268b9e521448b152e5f32a03b0 100644
--- a/iris/proofmode/coq_tactics.v
+++ b/iris/proofmode/coq_tactics.v
@@ -458,15 +458,51 @@ Proof.
 Qed.
 
 Class IntoIH (φ : Prop) (Δ : envs PROP) (Q : PROP) :=
-  into_ih : φ → of_envs Δ ⊢ Q.
+  into_ih : φ → □ of_envs Δ ⊢ Q.
 Global Instance into_ih_entails Δ Q : IntoIH (envs_entails Δ Q) Δ Q.
-Proof. by rewrite envs_entails_eq /IntoIH. Qed.
+Proof. by rewrite envs_entails_eq /IntoIH bi.intuitionistically_elim. Qed.
 Global Instance into_ih_forall {A} (φ : A → Prop) Δ Φ :
   (∀ x, IntoIH (φ x) Δ (Φ x)) → IntoIH (∀ x, φ x) Δ (∀ x, Φ x) | 2.
 Proof. rewrite /IntoIH=> HΔ ?. apply forall_intro=> x. by rewrite (HΔ x). Qed.
 Global Instance into_ih_impl (φ ψ : Prop) Δ Q :
   IntoIH φ Δ Q → IntoIH (ψ → φ) Δ (⌜ψ⌝ → Q) | 1.
 Proof. rewrite /IntoIH=> HΔ ?. apply impl_intro_l, pure_elim_l. auto. Qed.
+(** The instances [into_ih_Forall] and [into_ih_Forall2] are used to support
+induction principles for mutual inductive types such as finitely branching trees:
+
+  Inductive ntree := Tree : list ntree → ntree.
+
+  Lemma ntree_ind (P : ntree → Prop) :
+    (∀ l, Forall P l → P (Tree l)) → ∀ t, P t.
+
+Note 1: We need an [IntoIH] instance for any predicate transformer (like
+[Forall]) that is used in induction principles. However, since nested induction
+with lists is most common, we currently only support [Forall] and [Forall2].
+
+Note 2: We could also write the instance [into_ih_Forall] using the big operator
+for conjunction, or using the forall quantifier. We use the big operator
+because that corresponds most closely to [Forall], and we use the version with
+separating conjunction because we do not have a binary version of the big
+operator for conjunctions, and want to treat [Forall] and [Forall2]
+consistently. *)
+Global Instance into_ih_Forall {A} (φ : A → Prop) l Δ Φ :
+  (∀ x, IntoIH (φ x) Δ (Φ x)) →
+  IntoIH (Forall φ l) Δ ([∗ list] x ∈ l, □ Φ x) | 2.
+Proof.
+  rewrite /IntoIH=> HΔ. induction 1 as [|x l ? IH]; simpl.
+  { apply (affine _). }
+  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
+  apply intuitionistically_intro', HΔ; auto.
+Qed.
+Global Instance into_ih_Forall2 {A B} (φ : A → B → Prop) l1 l2 Δ Φ :
+  (∀ x1 x2, IntoIH (φ x1 x2) Δ (Φ x1 x2)) →
+  IntoIH (Forall2 φ l1 l2) Δ ([∗ list] x1;x2 ∈ l1;l2, □ Φ x1 x2) | 2.
+Proof.
+  rewrite /IntoIH=> HΔ. induction 1 as [|x1 x2 l1 l2 ? IH]; simpl.
+  { apply (affine _). }
+  rewrite {1}intuitionistically_sep_dup. f_equiv; [|done].
+  apply intuitionistically_intro', HΔ; auto.
+Qed.
 
 Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
   IntoIH φ Δ P →
@@ -476,8 +512,9 @@ Lemma tac_revert_ih Δ P Q {φ : Prop} (Hφ : φ) :
 Proof.
   rewrite /IntoIH envs_entails_eq. intros HP ? HPQ.
   rewrite (env_spatial_is_nil_intuitionistically Δ) //.
-  rewrite -(idemp bi_and (□ (of_envs Δ))%I) {1}HP // HPQ.
-  rewrite {1}intuitionistically_into_persistently_1 intuitionistically_elim impl_elim_r //.
+  rewrite -(idemp bi_and (□ (of_envs Δ))%I).
+  rewrite -{1}intuitionistically_idemp {1}intuitionistically_into_persistently_1.
+  by rewrite {1}HP // intuitionistically_elim HPQ impl_elim_r.
 Qed.
 
 Lemma tac_assert Δ j P Q :
diff --git a/iris/proofmode/ltac_tactics.v b/iris/proofmode/ltac_tactics.v
index 8bed1396997bb86d079524b4dbc5fa630011fd0d..f4da0ed786ded955e152a2d499e932b067b69484 100644
--- a/iris/proofmode/ltac_tactics.v
+++ b/iris/proofmode/ltac_tactics.v
@@ -2312,9 +2312,13 @@ Tactic Notation "iInductionCore" tactic3(tac) "as" constr(IH) :=
   let rec fix_ihs rev_tac :=
     lazymatch goal with
     | H : context [envs_entails _ _] |- _ =>
-       eapply (tac_revert_ih _ _ _ H _);
-         [pm_reflexivity
-          || fail "iInduction: spatial context not empty, this should not happen"
+       notypeclasses refine (tac_revert_ih _ _ _ H _ _ _);
+         [iSolveTC ||
+          let φ := match goal with |- IntoIH ?φ _ _ => φ end in
+          fail "iInduction: cannot import IH" φ
+               "into proof mode context (IntoIH instance missing)"
+         |pm_reflexivity ||
+          fail "iInduction: spatial context not empty, this should not happen"
          |clear H];
        fix_ihs ltac:(fun j =>
          let IH' := eval vm_compute in
diff --git a/tests/proofmode.ref b/tests/proofmode.ref
index cf81d3910ed4712dbb6a3e19df7e78f52cd00bf6..ce21d1c9d1c2c3b7629c0e461fa8a4ff09977bb1 100644
--- a/tests/proofmode.ref
+++ b/tests/proofmode.ref
@@ -790,3 +790,24 @@ Tactic failure: iIntuitionistic: "H" not fresh.
      : string
 The command has indeed failed with message:
 Tactic failure: iSpatial: "H" not fresh.
+"test_iInduction_Forall"
+     : string
+1 goal
+  
+  PROP : bi
+  P : ntree → PROP
+  l : list ntree
+  ============================
+  "H" : ∀ l0 : list ntree, (∀ x : ntree, ⌜x ∈ l0⌝ → P x) -∗ P (Tree l0)
+  "IH" : [∗ list] x ∈ l, □ P x
+  --------------------------------------â–¡
+  P (Tree l)
+"test_iInduction_Forall_fail"
+     : string
+The command has indeed failed with message:
+Tactic failure: iInduction: cannot import IH
+(my_Forall
+   (λ t : ntree,
+      "H" : ∀ l : list ntree, ([∗ list] x ∈ l, P x) -∗ P (Tree l)
+      --------------------------------------â–¡
+      P t) l) into proof mode context (IntoIH instance missing).
diff --git a/tests/proofmode.v b/tests/proofmode.v
index 7d9fecc09c9fc5dca2e5e46b24682c7926b36e57..b679d03e14ae48a0eba5a29687fb1a936b20cb4a 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -1712,3 +1712,63 @@ Proof.
 Abort.
 
 End tactic_tests.
+
+Section mutual_induction.
+  Context {PROP : bi}.
+  Implicit Types P Q R : PROP.
+  Implicit Types φ : nat → PROP.
+  Implicit Types Ψ : nat → nat → PROP.
+
+  Unset Elimination Schemes.
+  Inductive ntree := Tree : list ntree → ntree.
+
+  (** The common induction principle for finitely branching trees. By default,
+  Coq generates a too weak induction principle, so we have to prove it by hand. *)
+  Lemma ntree_ind (φ : ntree → Prop) :
+    (∀ l, Forall φ l → φ (Tree l)) →
+    ∀ t, φ t.
+  Proof.
+    intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
+    induction l as [|t l IH]; constructor; auto.
+  Qed.
+
+  (** Now let's test that we can derive the internal induction principle for
+  finitely branching trees in separation logic. There are many variants of the
+  induction principle, but we pick the variant with an induction hypothesis of
+  the form [∀ x, ⌜ x ∈ l ⌝ → ...]. This is most interesting, since the proof
+  mode generates a version with [[∗ list]]. *)
+  Check "test_iInduction_Forall".
+  Lemma test_iInduction_Forall (P : ntree → PROP) :
+    □ (∀ l, (∀ x, ⌜ x ∈ l ⌝ → P x) -∗ P (Tree l)) -∗
+    ∀ t, P t.
+  Proof.
+    iIntros "#H" (t). iInduction t as [] "IH".
+    Show. (* make sure that the induction hypothesis is exactly what we want *)
+    iApply "H". iIntros (x ?). by iApply (big_sepL_elem_of with "IH").
+  Qed.
+
+  (** Now let us define a custom version of [Forall], called [my_Forall], and
+  use that in the variant [ntree_ind_alt] of the induction principle. The proof
+  mode does not support [my_Forall], so we test if [iInduction] generates a
+  proper error message. *)
+  Inductive my_Forall {A} (φ : A → Prop) : list A → Prop :=
+    | my_Forall_nil : my_Forall φ []
+    | my_Forall_cons x l : φ x → my_Forall φ l → my_Forall φ (x :: l).
+
+  Lemma ntree_ind_alt (φ : ntree → Prop) :
+    (∀ l, my_Forall φ l → φ (Tree l)) →
+    ∀ t, φ t.
+  Proof.
+    intros Hrec. fix REC 1. intros [l]. apply Hrec. clear Hrec.
+    induction l as [|t l IH]; constructor; auto.
+  Qed.
+
+  Check "test_iInduction_Forall_fail".
+  Lemma test_iInduction_Forall_fail (P : ntree → PROP) :
+    □ (∀ l, ([∗ list] x ∈ l, P x) -∗ P (Tree l)) -∗
+    ∀ t, P t.
+  Proof.
+    iIntros "#H" (t).
+    Fail iInduction t as [] "IH" using ntree_ind_alt.
+  Abort.
+End mutual_induction.