instance Iris.BI.emp_intuitionistic {PROP : Type u_1} [BI PROP] : Intuitionistic iprop(emp)

instance Iris.BI.and_intuitionistic {PROP : Type u_1} [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuitionistic Q] : Intuitionistic iprop(P ∧ Q)

instance Iris.BI.or_intuitionistic {PROP : Type u_1} [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuitionistic Q] : Intuitionistic iprop(P ∨ Q)

instance Iris.BI.exists_intuitionistic {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) [∀ (x : α), Intuitionistic (Φ x)] : Intuitionistic («exists» fun (x : α) => Φ x)

instance Iris.BI.sep_intuitionistic {PROP : Type u_1} [BI PROP] (P Q : PROP) [Intuitionistic P] [Intuitionistic Q] : Intuitionistic iprop(P ∗ Q)

instance Iris.BI.intuitionistically_intuitionistic {PROP : Type u_1} [BI PROP] (P : PROP) : Intuitionistic iprop(□ P)