theorem Iris.Examples.proof_example_1 {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P Q R : PROP) (Φ : α → PROP) : P ∗ Q ∗ □ R ⊢ □ (R -∗ BI.exists fun (x : α) => Φ x) -∗ BI.exists fun (x : α) => iprop(Φ x ∗ P ∗ Q)