theorem Iris.ProofMode.false_elim_spatial {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ False ⊢ Q

theorem Iris.ProofMode.false_elim_intuitionistic {PROP : Type u_1} [BI PROP] {P Q : PROP} : P ∗ □ False ⊢ Q

theorem Iris.ProofMode.sep_emp_intro_spatial {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : P ∗ emp ⊢ Q

theorem Iris.ProofMode.sep_emp_intro_intuitionistic {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ Q) : P ∗ □ emp ⊢ Q

def Iris.ProofMode.iCasesEmptyConj {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) {P : Q(«$prop»)} (hyps : Hyps bi P) (Q A' : Q(«$prop»)) (p : Q(Bool)) (k : {P : Q(«$prop»)} → Hyps bi P → Lean.MetaM Q(«$P» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.exists_elim_spatial {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P A Q : PROP} {Φ : α → PROP} [inst : IntoExists A Φ] (h : ∀ (a : α), P ∗ Φ a ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.exists_elim_intuitionistic {PROP : Type u_1} {α : Sort u_2} [BI PROP] {P A Q : PROP} {Φ : α → PROP} [IntoExists A Φ] (h : ∀ (a : α), P ∗ □ Φ a ⊢ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesExists {u v : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P Q A' : Q(«$prop»)) (p : Q(Bool)) (name : Lean.TSyntax `Lean.binderIdent) (α : Q(Sort v)) (Φ : Q(«$α» → «$prop»)) (_inst : Q(IntoExists «$A'» «$Φ»)) (k : (B B' : Q(«$prop»)) → «$B» =Q iprop(□?«$p» «$B'») → Lean.MetaM Q(«$P» ∗ «$B» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.sep_and_elim_l {PROP : Type u_1} {p : Bool} [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] (h : P ∗ □?p A1 ⊢ Q) : P ∗ □?p A ⊢ Q

theorem Iris.ProofMode.and_elim_l_spatial {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2] (h : P ∗ A1 ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.and_elim_l_intuitionistic {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd true A A1 A2] (h : P ∗ □ A1 ⊢ Q) : P ∗ □ A ⊢ Q

theorem Iris.ProofMode.sep_and_elim_r {PROP : Type u_1} {p : Bool} [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd p A A1 A2] (h : P ∗ □?p A2 ⊢ Q) : P ∗ □?p A ⊢ Q

theorem Iris.ProofMode.and_elim_r_spatial {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd false A A1 A2] (h : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.and_elim_r_intuitionistic {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [IntoAnd true A A1 A2] (h : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesAndLR {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P Q A' A1 A2 : Q(«$prop»)) (p : Q(Bool)) (_inst : Q(IntoAnd «$p» «$A'» «$A1» «$A2»)) (right : Bool) (k : (B B' : Q(«$prop»)) → «$B» =Q iprop(□?«$p» «$B'») → Lean.MetaM Q(«$P» ∗ «$B» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.sep_elim_spatial {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoSep A A1 A2] (h : P ∗ A1 ⊢ A2 -∗ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.and_elim_intuitionistic {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoAnd true A A1 A2] (h : P ∗ □ A1 ⊢ □ A2 -∗ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesSep {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) {P : Q(«$prop»)} (hyps : Hyps bi P) (Q A' A1 A2 : Q(«$prop»)) (p : Q(Bool)) (inst : Option Q(IntoAnd «$p» «$A'» «$A1» «$A2»)) (k : {P : Q(«$prop»)} → Hyps bi P → Lean.MetaM Q(«$P» ⊢ «$Q»)) (k1 k2 : {P : Q(«$prop»)} → Hyps bi P → (Q B B' : Q(«$prop»)) → «$B» =Q iprop(□?«$p» «$B'») → ({P : Q(«$prop»)} → Hyps bi P → Lean.MetaM Q(«$P» ⊢ «$Q»)) → Lean.MetaM Q(«$P» ∗ «$B» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.or_elim_spatial {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [inst : IntoOr A A1 A2] (h1 : P ∗ A1 ⊢ Q) (h2 : P ∗ A2 ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.or_elim_intuitionistic {PROP : Type u_1} [BI PROP] {P A Q A1 A2 : PROP} [IntoOr A A1 A2] (h1 : P ∗ □ A1 ⊢ Q) (h2 : P ∗ □ A2 ⊢ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesOr {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P Q A' : Q(«$prop»)) (p : Q(Bool)) (k1 k2 : (B B' : Q(«$prop»)) → «$B» =Q iprop(□?«$p» «$B'») → Lean.MetaM Q(«$P» ∗ «$B» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.intuitionistic_elim_spatial {PROP : Type u_1} {P : PROP} [BI PROP] {A A' Q : PROP} [IntoPersistently false A A'] [Std.TCOr (BI.Affine A) (BI.Absorbing Q)] (h : P ∗ □ A' ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.intuitionistic_elim_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] {A A' Q : PROP} [IntoPersistently true A A'] (h : P ∗ □ A' ⊢ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesIntuitionistic {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P Q A' : Q(«$prop»)) (p : Q(Bool)) (k : (B' : Q(«$prop»)) → Lean.MetaM Q(«$P» ∗ □ «$B'» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.spatial_elim_spatial {PROP : Type u_1} {P : PROP} [BI PROP] {A A' Q : PROP} [FromAffinely A' A false] (h : P ∗ A' ⊢ Q) : P ∗ A ⊢ Q

theorem Iris.ProofMode.spatial_elim_intuitionistic {PROP : Type u_1} {P : PROP} [BI PROP] {A A' Q : PROP} [FromAffinely A' A] (h : P ∗ A' ⊢ Q) : P ∗ □ A ⊢ Q

def Iris.ProofMode.iCasesSpatial {u : Lean.Level} {prop : Q(Type u)} (_bi : Q(BI «$prop»)) (P Q A' : Q(«$prop»)) (p : Q(Bool)) (k : (B' : Q(«$prop»)) → Lean.MetaM Q(«$P» ∗ «$B'» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ∗ □?«$p» «$A'» ⊢ «$Q»)

Equations

• One or more equations did not get rendered due to their size.

theorem Iris.ProofMode.of_emp_sep {PROP : Type u_1} [BI PROP] {A Q : PROP} (h : A ⊢ Q) : emp ∗ A ⊢ Q

partial def Iris.ProofMode.iCasesCore {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) {P : Q(«$prop»)} (hyps : Hyps bi P) (Q : Q(«$prop»)) (p : Q(Bool)) (A A' : Q(«$prop»)) : «$A» =Q iprop(□?«$p» «$A'») → (pat : iCasesPat) → (k : {P : Q(«$prop»)} → Hyps bi P → Lean.MetaM Q(«$P» ⊢ «$Q»)) → Lean.MetaM Q(«$P» ∗ «$A» ⊢ «$Q»)

def Iris.ProofMode.tacticIcases__With__ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.