#### The one place for your designs

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.

The "flattened" introduction patterns (I don't know the official terminology, but I meant the patterns like `(H1 & H2 & H3 &H4)`

) interact in a weird way with intuitionistic conjunction:

In particular, I would expect to get a `P`

from `P ∧ Q ∧ R`

by `iDestruct "H" as "(H&_&_)"`

, but it doesn't work this way.

```
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic.
Section base_logic_tests.
Context {M : ucmraT}.
Implicit Types P Q R : uPred M.
Lemma test P Q R : (P ∧ Q ∧ R) -∗ P.
Proof.
iIntros "H".
(* This works fine *)
iDestruct "H" as "(_ & _ & H)".
Undo.
iDestruct "H" as "(_ & H & _)".
Undo.
(* This results in an error *)
Fail iDestruct "H" as "(H & _ & _)".
(* "Proper" way of doing it *)
iDestruct "H" as "(H & _)".
done.
Qed.
```

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.