diff --git a/iris/proofmode/class_instances.v b/iris/proofmode/class_instances.v
index 90e639c963cbfce5838edfad2a26a6cf2fca98c2..d28a5f9d170475c0b38116dfaf7a54c5a13f20c7 100644
--- a/iris/proofmode/class_instances.v
+++ b/iris/proofmode/class_instances.v
@@ -608,9 +608,9 @@ Proof.
   rewrite /IntoAnd /= intuitionistically_sep
     -and_sep_intuitionistically intuitionistically_and //.
 Qed.
-Global Instance into_and_sep_affine P Q :
+Global Instance into_and_sep_affine p P Q :
   TCOr (Affine P) (Absorbing Q) → TCOr (Absorbing P) (Affine Q) →
-  IntoAnd true (P ∗ Q) P Q.
+  IntoAnd p (P ∗ Q) P Q.
 Proof. intros. by rewrite /IntoAnd /= sep_and. Qed.
 
 Global Instance into_and_pure p φ ψ : @IntoAnd PROP p ⌜φ ∧ ψ⌝ ⌜φ⌝ ⌜ψ⌝.
@@ -807,32 +807,32 @@ Proof. rewrite /IntoExist=> HP. by rewrite HP affinely_exist. Qed.
 Global Instance into_exist_intuitionistically {A} P (Φ : A → PROP) name :
   IntoExist P Φ name → IntoExist (□ P) (λ a, □ (Φ a))%I name.
 Proof. rewrite /IntoExist=> HP. by rewrite HP intuitionistically_exist. Qed.
-(* Low-priority instance falling back to treating a conjunction with a pure
-left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
-[% ...]].
+(* This instance is generalized to let us use [iIntros (P) "..."] and
+[as [% ...]]. There is some risk of backtracking here, but that should only
+happen in failing cases (assuming that appropriate modality commuting instances
+are provided for both conjunctions and existential quantification). The
+alternative of providing specialized instances for cases like ⌜P ∧ Q⌝ turned out
+to not be tenable.
+
 [to_ident_name H] makes the default name [H] when [P] is destructed with
-[iExistDestruct] *)
-Global Instance into_exist_and_pure PQ P Q φ :
+[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
+Global Instance into_exist_and_pure PQ P Q (φ : Type) :
   IntoAnd false PQ P Q →
   IntoPureT P φ →
-  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
+  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 10.
 Proof.
   intros HPQ (φ'&->&?). rewrite /IntoAnd /= in HPQ.
   rewrite /IntoExist HPQ (into_pure P).
   apply pure_elim_l=> Hφ. by rewrite -(exist_intro Hφ).
 Qed.
-(* Low-priority instance falling back to treating a sep. conjunction with a pure
-left-hand side as an existential. This lets us use [iIntros (P) "..."] and [as
-[% ...]].
-[to_ident_name H] makes the default name [H] when [P] is destructed with
-[iExistDestruct] *)
-Global Instance into_exist_sep_pure PQ P Q φ :
-  IntoSep PQ P Q →
+(* [to_ident_name H] makes the default name [H] when [P] is destructed with
+[iExistDestruct]. See [IntoPureT] for why [φ] is a [Type]. *)
+Global Instance into_exist_sep_pure P Q (φ : Type) :
   IntoPureT P φ →
   TCOr (Affine P) (Absorbing Q) →
-  IntoExist PQ (λ _ : φ, Q) (to_ident_name H) | 100.
+  IntoExist (P ∗ Q) (λ _ : φ, Q) (to_ident_name H).
 Proof.
-  intros HPQ (φ'&->&?) ?. rewrite /IntoSep in HPQ. rewrite /IntoExist HPQ.
+  intros (φ'&->&?) ?. rewrite /IntoExist.
   eapply (pure_elim φ'); [by rewrite (into_pure P); apply sep_elim_l, _|]=>?.
   rewrite -exist_intro //. apply sep_elim_r, _.
 Qed.
diff --git a/iris/proofmode/classes.v b/iris/proofmode/classes.v
index f4e72648388f18150bc14d1cde425b0201488ba8..74472b17b9e072ba3c8f430d718015655964a1b6 100644
--- a/iris/proofmode/classes.v
+++ b/iris/proofmode/classes.v
@@ -176,12 +176,21 @@ Global Arguments from_and {_} _%I _%I _%I {_}.
 Global Hint Mode FromAnd + ! - - : typeclass_instances.
 Global Hint Mode FromAnd + - ! ! : typeclass_instances. (* For iCombine *)
 
+(** The [IntoAnd p P Q1 Q2] class is used (together with [IntoSep]) to handle
+[[H1 H2]] destruct patterns. If [p] is [true] then the destruct is happening in
+the intuitionistic context.
+
+The inputs are [p P] and the outputs are [Q1 Q2]. *)
 Class IntoAnd {PROP : bi} (p : bool) (P Q1 Q2 : PROP) :=
   into_and : □?p P ⊢ □?p (Q1 ∧ Q2).
 Global Arguments IntoAnd {_} _ _%I _%I _%I : simpl never.
 Global Arguments into_and {_} _ _%I _%I _%I {_}.
 Global Hint Mode IntoAnd + + ! - - : typeclass_instances.
 
+(** The [IntoSep P Q1 Q2] class is used (together with [IntoAnd]) to handle
+[[H1 H2]] destruct patterns.
+
+The input is [P] and the outputs are [Q1 Q2]. *)
 Class IntoSep {PROP : bi} (P Q1 Q2 : PROP) :=
   into_sep : P ⊢ Q1 ∗ Q2.
 Global Arguments IntoSep {_} _%I _%I _%I : simpl never.