@[instance 990]

instance Iris.ProofMode.asEmpValidEmpValid1 {PROP : Type u_1} [BI PROP] (P : PROP) : AsEmpValid1 (⊢ P) P

@[instance 1010]

instance Iris.ProofMode.asEmpValidEmpValid2 {PROP : Type u_1} [BI PROP] (P : PROP) : AsEmpValid2 (⊢ P) P

instance Iris.ProofMode.asEmpValid1_entails {PROP : Type u_1} [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊢ Q) iprop(P -∗ Q)

instance Iris.ProofMode.asEmpValid2_entails {PROP : Type u_1} [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊢ Q) iprop(P -∗ Q)

instance Iris.ProofMode.asEmpValid1_equiv {PROP : Type u_1} [BI PROP] (P Q : PROP) : AsEmpValid1 (P ⊣⊢ Q) iprop(P ∗-∗ Q)

instance Iris.ProofMode.asEmpValid2_equiv {PROP : Type u_1} [BI PROP] (P Q : PROP) : AsEmpValid2 (P ⊣⊢ Q) iprop(P ∗-∗ Q)

instance Iris.ProofMode.fromImp_imp {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) : FromImp iprop(P1 → P2) P1 P2

instance Iris.ProofMode.fromWand_wand {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) : FromWand iprop(P1 -∗ P2) P1 P2

instance Iris.ProofMode.intoWand_wand {PROP : Type u_1} (p q : Bool) [BI PROP] (P Q P' : PROP) [h : FromAssumption q P P'] : IntoWand p q iprop(P' -∗ Q) P Q

instance Iris.ProofMode.intoWand_imp_false {PROP : Type u_1} {b : Bool} [BI PROP] (P Q P' : PROP) [BI.Absorbing P'] [BI.Absorbing iprop(P' → Q)] [h : FromAssumption b P P'] : IntoWand false b iprop(P' → Q) P Q

instance Iris.ProofMode.intoWand_imp_true {PROP : Type u_1} {b : Bool} [BI PROP] (P Q P' : PROP) [BI.Affine P'] [h : FromAssumption b P P'] : IntoWand true b iprop(P' → Q) P Q

instance Iris.ProofMode.intoWand_and_l {PROP : Type u_1} (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP) [h : IntoWand p q R1 P' Q'] : IntoWand p q iprop(R1 ∧ R2) P' Q'

instance Iris.ProofMode.intoWand_and_r {PROP : Type u_1} (p q : Bool) [BI PROP] (R1 R2 P' Q' : PROP) [h : IntoWand p q R2 Q' P'] : IntoWand p q iprop(R1 ∧ R2) Q' P'

instance Iris.ProofMode.intoWand_forall {PROP : Type u_1} {α : Sort u_2} (p q : Bool) [BI PROP] (Φ : α → PROP) (P Q : PROP) (x : α) [h : IntoWand p q (Φ x) P Q] : IntoWand p q (BI.forall fun (x : α) => Φ x) P Q

instance Iris.ProofMode.intoWand_affinely {PROP : Type u_1} (p q : Bool) [BI PROP] (R P Q : PROP) [h : IntoWand p q R P Q] : IntoWand p q iprop(<affine> R) iprop(<affine> P) iprop(<affine> Q)

instance Iris.ProofMode.intoWand_intuitionistically {PROP : Type u_1} (p q : Bool) [BI PROP] (R P Q : PROP) [h : IntoWand true q R P Q] : IntoWand p q iprop(□ R) P Q

instance Iris.ProofMode.intoWand_persistently_true {PROP : Type u_1} (q : Bool) [BI PROP] (R P Q : PROP) [h : IntoWand true q R P Q] : IntoWand true q iprop(<pers> R) P Q

instance Iris.ProofMode.intoWand_persistently_false {PROP : Type u_1} (q : Bool) [BI PROP] (R P Q : PROP) [BI.Absorbing R] [h : IntoWand false q R P Q] : IntoWand false q iprop(<pers> R) P Q

instance Iris.ProofMode.fromForall_forall {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) : FromForall (BI.forall Φ) Φ

instance Iris.ProofMode.intoForall_forall {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) : IntoForall (BI.forall fun (a : α) => Φ a) Φ

instance Iris.ProofMode.intoForall_affinely {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoForall P Φ] : IntoForall iprop(<affine> P) fun (a : α) => iprop(<affine> Φ a)

instance Iris.ProofMode.intoForall_intuitionistically {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoForall P Φ] : IntoForall iprop(□ P) fun (a : α) => iprop(□ Φ a)

@[instance 1010]

instance Iris.ProofMode.fromExists_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) : FromExists (BI.exists fun (a : α) => Φ a) Φ

instance Iris.ProofMode.fromExists_pure {α : Sort u_1} {PROP : Type u_2} (φ : α → Prop) [BI PROP] : FromExists iprop(⌜∃ (x : α), φ x⌝) fun (a : α) => iprop(⌜φ a⌝)

instance Iris.ProofMode.fromExists_affinely {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] : FromExists iprop(<affine> P) fun (a : α) => iprop(<affine> Φ a)

instance Iris.ProofMode.fromExists_intuitionistically {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] : FromExists iprop(□ P) fun (a : α) => iprop(□ Φ a)

instance Iris.ProofMode.fromExists_absorbingly {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] : FromExists iprop(<absorb> P) fun (a : α) => iprop(<absorb> Φ a)

instance Iris.ProofMode.fromExists_persistently {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : FromExists P Φ] : FromExists iprop(<pers> P) fun (a : α) => iprop(<pers> Φ a)

instance Iris.ProofMode.intoExists_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) : IntoExists (BI.exists Φ) Φ

instance Iris.ProofMode.intoExists_pure {α : Sort u_1} {PROP : Type u_2} (φ : α → Prop) [BI PROP] : IntoExists iprop(⌜∃ (x : α), φ x⌝) fun (a : α) => iprop(⌜φ a⌝)

instance Iris.ProofMode.intoExists_affinely {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] : IntoExists iprop(<affine> P) fun (a : α) => iprop(<affine> Φ a)

instance Iris.ProofMode.intoExists_intuitionistically {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] : IntoExists iprop(□ P) fun (a : α) => iprop(□ Φ a)

instance Iris.ProofMode.intoExists_absorbingly {PROP : Type u_1} {α : Sort u_2} [BI PROP] (P : PROP) (Φ : α → PROP) [h : IntoExists P Φ] : IntoExists iprop(<absorb> P) fun (a : α) => iprop(<absorb> Φ a)

instance Iris.ProofMode.intoExists_persistently {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P : PROP} (Φ : α → PROP) [h : IntoExists P Φ] : IntoExists iprop(<pers> P) fun (a : α) => iprop(<pers> Φ a)

@[instance 990]

instance Iris.ProofMode.fromAnd_and {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) : FromAnd iprop(P1 ∧ P2) P1 P2

@[instance 1030]

instance Iris.ProofMode.fromAnd_sep_persistent_l {PROP : Type u_1} [BI PROP] (P1 P1' P2 : PROP) [BI.Persistent P1] [h : IntoAbsorbingly P1' P1] : FromAnd iprop(P1 ∗ P2) P1' P2

@[instance 1020]

instance Iris.ProofMode.fromAnd_sep_persistent_r {PROP : Type u_1} [BI PROP] (P1 P2 P2' : PROP) [BI.Persistent P2] [h : IntoAbsorbingly P2' P2] : FromAnd iprop(P1 ∗ P2) P1 P2'

@[instance 1050]

instance Iris.ProofMode.fromAnd_pure {PROP : Type u_1} (φ ψ : Prop) [BI PROP] : FromAnd iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

@[instance 1040]

instance Iris.ProofMode.fromAnd_persistently {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromAnd P Q1 Q2] : FromAnd iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

@[instance 1010]

instance Iris.ProofMode.fromAnd_persistently_sep {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromSep P Q1 Q2] : FromAnd iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

@[instance 990]

instance Iris.ProofMode.intoAnd_and {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) : IntoAnd p iprop(P ∧ Q) P Q

instance Iris.ProofMode.intoAnd_and_affine_l {PROP : Type u_1} [BI PROP] (P Q Q' : PROP) [BI.Affine P] [h : FromAffinely Q' Q] : IntoAnd false iprop(P ∧ Q) P Q'

instance Iris.ProofMode.intoAnd_and_affine_r {PROP : Type u_1} [BI PROP] (P P' Q : PROP) [BI.Affine Q] [h : FromAffinely P' P] : IntoAnd false iprop(P ∧ Q) P' Q

instance Iris.ProofMode.intoAnd_sep_affine {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [Std.TCOr (BI.Affine P) (BI.Absorbing Q)] [Std.TCOr (BI.Affine Q) (BI.Absorbing P)] : IntoAnd p iprop(P ∗ Q) P Q

instance Iris.ProofMode.intoAnd_pure {PROP : Type u_1} (p : Bool) (φ ψ : Prop) [BI PROP] : IntoAnd p iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

instance Iris.ProofMode.intoAnd_affinely {PROP : Type u_1} (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] : IntoAnd p iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2)

instance Iris.ProofMode.intoAnd_intuitionistically {PROP : Type u_1} (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] : IntoAnd p iprop(□ P) iprop(□ Q1) iprop(□ Q2)

instance Iris.ProofMode.intoAnd_persistently {PROP : Type u_1} (p : Bool) [BI PROP] (P Q1 Q2 : PROP) [h : IntoAnd p P Q1 Q2] : IntoAnd p iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

@[instance 990]

instance Iris.ProofMode.fromSep_sep {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) : FromSep iprop(P1 ∗ P2) P1 P2

@[instance 980]

instance Iris.ProofMode.fromSep_and {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) [Std.TCOr (BI.Affine P1) (BI.Absorbing P2)] [Std.TCOr (BI.Affine P2) (BI.Absorbing P1)] : FromSep iprop(P1 ∧ P2) P1 P2

@[instance 1020]

instance Iris.ProofMode.fromSep_pure {PROP : Type u_1} (φ ψ : Prop) [BI PROP] : FromSep iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

@[instance 1010]

instance Iris.ProofMode.fromSep_affinely {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromSep P Q1 Q2] : FromSep iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2)

@[instance 1010]

instance Iris.ProofMode.fromSep_intuitionistically {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromSep P Q1 Q2] : FromSep iprop(□ P) iprop(□ Q1) iprop(□ Q2)

@[instance 1010]

instance Iris.ProofMode.fromSep_absorbingly {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromSep P Q1 Q2] : FromSep iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2)

@[instance 1010]

instance Iris.ProofMode.fromSep_persistently {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromSep P Q1 Q2] : FromSep iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

class inductive Iris.ProofMode.AndIntoSep {PROP : Type u_1} [BI PROP] : PROP → PROP → PROP → PROP → Prop

• affine {PROP : Type u_1} [BI PROP] (P Q Q' : PROP) [BI.Affine P] [h : FromAffinely Q' Q] : AndIntoSep P P Q Q'
• affinely {PROP : Type u_1} [BI PROP] (P Q : PROP) : AndIntoSep P iprop(<affine> P) Q Q

instance Iris.ProofMode.intoSep_sep {PROP : Type u_1} [BI PROP] (P Q : PROP) : IntoSep iprop(P ∗ Q) P Q

instance Iris.ProofMode.intoSep_and_persistent_l {PROP : Type u_1} [BI PROP] (P Q P' Q' : PROP) [BI.Persistent P] [inst : AndIntoSep P P' Q Q'] : IntoSep iprop(P ∧ Q) P' Q'

instance Iris.ProofMode.intoSep_and_persistent_r {PROP : Type u_1} [BI PROP] (P Q P' Q' : PROP) [BI.Persistent Q] [inst : AndIntoSep Q Q' P P'] : IntoSep iprop(P ∧ Q) P' Q'

instance Iris.ProofMode.intoSep_pure {PROP : Type u_1} (φ ψ : Prop) [BI PROP] : IntoSep iprop(⌜φ ∧ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

@[instance 990]

instance Iris.ProofMode.intoSep_affinely_trim {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2] : IntoSep iprop(<affine> P) Q1 Q2

instance Iris.ProofMode.intoSep_persistently_affine {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2] [Std.TCOr (BI.Affine Q1) (BI.Absorbing Q2)] [Std.TCOr (BI.Affine Q2) (BI.Absorbing Q1)] : IntoSep iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

instance Iris.ProofMode.intoSep_intuitionistically_affine {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoSep P Q1 Q2] [Std.TCOr (BI.Affine Q1) (BI.Absorbing Q2)] [Std.TCOr (BI.Affine Q2) (BI.Absorbing Q1)] : IntoSep iprop(□ P) iprop(□ Q1) iprop(□ Q2)

instance Iris.ProofMode.fromOr_or {PROP : Type u_1} [BI PROP] (P1 P2 : PROP) : FromOr iprop(P1 ∨ P2) P1 P2

instance Iris.ProofMode.fromOr_pure {PROP : Type u_1} (φ ψ : Prop) [BI PROP] : FromOr iprop(⌜φ ∨ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

instance Iris.ProofMode.fromOr_affinely {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] : FromOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2)

instance Iris.ProofMode.fromOr_intuitionistically {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] : FromOr iprop(□ P) iprop(□ Q1) iprop(□ Q2)

instance Iris.ProofMode.fromOr_absorbingly {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] : FromOr iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2)

instance Iris.ProofMode.fromOr_persistently {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : FromOr P Q1 Q2] : FromOr iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

instance Iris.ProofMode.intoOr_or {PROP : Type u_1} [BI PROP] (P Q : PROP) : IntoOr iprop(P ∨ Q) P Q

instance Iris.ProofMode.intoOr_pure {PROP : Type u_1} (φ ψ : Prop) [BI PROP] : IntoOr iprop(⌜φ ∨ ψ⌝) iprop(⌜φ⌝) iprop(⌜ψ⌝)

instance Iris.ProofMode.intoOr_affinely {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] : IntoOr iprop(<affine> P) iprop(<affine> Q1) iprop(<affine> Q2)

instance Iris.ProofMode.intoOr_intuitionistically {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] : IntoOr iprop(□ P) iprop(□ Q1) iprop(□ Q2)

instance Iris.ProofMode.intoOr_absorbingly {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] : IntoOr iprop(<absorb> P) iprop(<absorb> Q1) iprop(<absorb> Q2)

instance Iris.ProofMode.intoOr_persistently {PROP : Type u_1} [BI PROP] (P Q1 Q2 : PROP) [h : IntoOr P Q1 Q2] : IntoOr iprop(<pers> P) iprop(<pers> Q1) iprop(<pers> Q2)

@[instance 1020]

instance Iris.ProofMode.intoPersistently_persistently {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : IntoPersistently true P Q] : IntoPersistently p iprop(<pers> P) Q

@[instance 1020]

instance Iris.ProofMode.intoPersistently_affinely {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : IntoPersistently p P Q] : IntoPersistently p iprop(<affine> P) Q

@[instance 1020]

instance Iris.ProofMode.intoPersistently_intuitionistically {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : IntoPersistently true P Q] : IntoPersistently p iprop(□ P) Q

@[instance 1010]

instance Iris.ProofMode.intoPersistently_self {PROP : Type u_1} [BI PROP] (P : PROP) : IntoPersistently true P P

@[instance 990]

instance Iris.ProofMode.intoPersistently_persistent {PROP : Type u_1} [BI PROP] (P : PROP) [h : BI.Persistent P] : IntoPersistently false P P

instance Iris.ProofMode.fromAffinely_affine {PROP : Type u_1} [BI PROP] (P : PROP) [BI.Affine P] : FromAffinely P P

@[instance 950]

instance Iris.ProofMode.fromAffinely_affinely {PROP : Type u_1} [BI PROP] (P : PROP) : FromAffinely iprop(<affine> P) P

@[instance 990]

instance Iris.ProofMode.fromAffinely_intuitionistically {PROP : Type u_1} [BI PROP] (P : PROP) : FromAffinely iprop(□ P) iprop(<pers> P)

instance Iris.ProofMode.fromAffinely_self {PROP : Type u_1} [BI PROP] (P : PROP) : FromAffinely P P false

@[instance 1030]

instance Iris.ProofMode.intoAbsorbingly_true {PROP : Type u_1} [BI PROP] : IntoAbsorbingly iprop(True) iprop(emp)

@[instance 1020]

instance Iris.ProofMode.intoAbsorbingly_absorbing {PROP : Type u_1} [BI PROP] (P : PROP) [BI.Absorbing P] : IntoAbsorbingly P P

@[instance 1010]

instance Iris.ProofMode.intoAbsorbingly_intuitionistically {PROP : Type u_1} [BI PROP] (P : PROP) : IntoAbsorbingly iprop(<pers> P) iprop(□ P)

@[instance 990]

instance Iris.ProofMode.intoAbsorbingly_default {PROP : Type u_1} [BI PROP] (P : PROP) : IntoAbsorbingly iprop(<absorb> P) P

@[instance 1100]

instance Iris.ProofMode.fromAssumption_exact {PROP : Type u_1} (p : Bool) [BI PROP] (P : PROP) : FromAssumption p P P

@[instance 1030]

instance Iris.ProofMode.fromAssumption_persistently_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption true P iprop(<pers> Q)

@[instance 1030]

instance Iris.ProofMode.fromAssumption_affinely_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption true P iprop(<affine> Q)

@[instance 1030]

instance Iris.ProofMode.fromAssumption_intuitionistically_r {PROP : Type u_1} [BI PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption true P iprop(□ Q)

@[instance 1020]

instance Iris.ProofMode.fromAssumption_absorbingly_r {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : FromAssumption p P Q] : FromAssumption p P iprop(<absorb> Q)

@[instance 1020]

instance Iris.ProofMode.fromAssumption_intuitionistically_l {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption p iprop(□ P) Q

@[instance 1020]

instance Iris.ProofMode.fromAssumption_intuitionistically_l_true {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : FromAssumption p P Q] : FromAssumption p iprop(□ P) Q

@[instance 1030]

instance Iris.ProofMode.fromAssumption_persistently_l_true {PROP : Type u_1} [BI PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption true iprop(<pers> P) Q

@[instance 1030]

instance Iris.ProofMode.fromAssumption_persistently_l_false {PROP : Type u_1} [BI PROP] [BI.BIAffine PROP] (P Q : PROP) [h : FromAssumption true P Q] : FromAssumption false iprop(<pers> P) Q

@[instance 1020]

instance Iris.ProofMode.fromAssumption_affinely_l {PROP : Type u_1} (p : Bool) [BI PROP] (P Q : PROP) [h : FromAssumption p P Q] : FromAssumption p iprop(<affine> P) Q

@[instance 1010]

instance Iris.ProofMode.fromAssumption_forall {PROP : Type u_1} {α : Sort u_2} (p : Bool) [BI PROP] (Φ : α → PROP) (x : α) (Q : PROP) [h : FromAssumption p (Φ x) Q] : FromAssumption p (BI.forall fun (x : α) => Φ x) Q

instance Iris.ProofMode.intoPure_pure {PROP : Type u_1} (φ : Prop) [BI PROP] : IntoPure iprop(⌜φ⌝) φ

instance Iris.ProofMode.intoPure_pure_and {PROP : Type u_1} (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∧ P2) (φ1 ∧ φ2)

instance Iris.ProofMode.intoPure_pure_or {PROP : Type u_1} (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∨ P2) (φ1 ∨ φ2)

instance Iris.ProofMode.intoPure_exists {PROP : Type u_1} {α : Sort u_2} [BI PROP] (Φ : α → PROP) (φ : α → Prop) [h : ∀ (x : α), IntoPure (Φ x) (φ x)] : IntoPure (BI.exists fun (x : α) => Φ x) (∃ (x : α), φ x)

instance Iris.ProofMode.intoPure_pure_sep {PROP : Type u_1} (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : IntoPure P2 φ2] : IntoPure iprop(P1 ∗ P2) (φ1 ∧ φ2)

instance Iris.ProofMode.intoPure_affinely {PROP : Type u_1} [BI PROP] (P : PROP) (φ : Prop) [h : IntoPure P φ] : IntoPure iprop(<affine> P) φ

instance Iris.ProofMode.intoPure_intuitionistically {PROP : Type u_1} [BI PROP] (P : PROP) (φ : Prop) [h : IntoPure P φ] : IntoPure iprop(□ P) φ

instance Iris.ProofMode.intoPure_absorbingly {PROP : Type u_1} [BI PROP] (P : PROP) (φ : Prop) [h : IntoPure P φ] : IntoPure iprop(<absorb> P) φ

instance Iris.ProofMode.intoPure_persistently {PROP : Type u_1} [BI PROP] (P : PROP) (φ : Prop) [h : IntoPure P φ] : IntoPure iprop(<pers> P) φ

instance Iris.ProofMode.fromPure_emp {PROP : Type u_1} [BI PROP] : FromPure true iprop(emp) True

instance Iris.ProofMode.fromPure_pure {PROP : Type u_1} [BI PROP] (φ : Prop) : FromPure false iprop(⌜φ⌝) φ

instance Iris.ProofMode.fromPure_pure_and {PROP : Type u_1} (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : FromPure a1 P1 φ1] [h2 : FromPure a2 P2 φ2] : FromPure (a1 || a2) iprop(P1 ∧ P2) (φ1 ∧ φ2)

instance Iris.ProofMode.fromPure_pure_or {PROP : Type u_1} (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : FromPure a1 P1 φ1] [h2 : FromPure a2 P2 φ2] : FromPure (a1 || a2) iprop(P1 ∨ P2) (φ1 ∨ φ2)

instance Iris.ProofMode.fromPure_pure_imp {PROP : Type u_1} (a : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : FromPure a P2 φ2] : FromPure a iprop(P1 → P2) (φ1 → φ2)

instance Iris.ProofMode.fromPure_exists {PROP : Type u_1} {α : Sort u_2} (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop) [h : ∀ (x : α), FromPure a (Φ x) (φ x)] : FromPure a (BI.exists fun (x : α) => Φ x) (∃ (x : α), φ x)

instance Iris.ProofMode.fromPure_forall {PROP : Type u_1} {α : Sort u_2} (a : Bool) [BI PROP] (Φ : α → PROP) (φ : α → Prop) [h : ∀ (x : α), FromPure a (Φ x) (φ x)] : FromPure a (BI.forall fun (x : α) => Φ x) (∀ (x : α), φ x)

instance Iris.ProofMode.fromPure_pure_sep_true {PROP : Type u_1} (a1 a2 : Bool) (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : FromPure a1 P1 φ1] [h2 : FromPure a2 P2 φ2] : FromPure (a1 && a2) iprop(P1 ∗ P2) (φ1 ∧ φ2)

instance Iris.ProofMode.fromPure_pure_wand_true {PROP : Type u_1} (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : FromPure true P2 φ2] [BI.Affine P1] : FromPure true iprop(P1 -∗ P2) (φ1 → φ2)

instance Iris.ProofMode.fromPure_pure_wand_false {PROP : Type u_1} (φ1 φ2 : Prop) [BI PROP] (P1 P2 : PROP) [h1 : IntoPure P1 φ1] [h2 : FromPure false P2 φ2] : FromPure false iprop(P1 -∗ P2) (φ1 → φ2)

instance Iris.ProofMode.fromPure_persistently {PROP : Type u_1} [BI PROP] (P : PROP) (a : Bool) (φ : Prop) [h : FromPure true P φ] : FromPure a iprop(<pers> P) φ

instance Iris.ProofMode.fromPure_affinely_true {PROP : Type u_1} (a : Bool) [BI PROP] (P : PROP) (φ : Prop) [h : FromPure a P φ] : FromPure true iprop(<affine> P) φ

instance Iris.ProofMode.fromPure_intuitionistically_true {PROP : Type u_1} (a : Bool) [BI PROP] (P : PROP) (φ : Prop) [h : FromPure a P φ] : FromPure true iprop(□ P) φ

instance Iris.ProofMode.fromPure_absorbingly {PROP : Type u_1} (a : Bool) [BI PROP] (P : PROP) (φ : Prop) [h : FromPure a P φ] : FromPure false iprop(<absorb> P) φ