theorem Iris.ProofMode.imp_intro_drop {PROP : Type u_1} [BI PROP] {P Q A1 A2 : PROP} [inst : FromImp Q A1 A2] (h : P ⊢ A2) : P ⊢ Q

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

theorem Iris.ProofMode.imp_intro_intuitionistic {PROP : Type u_1} [BI PROP] {P Q A1 A2 B : PROP} [FromImp Q A1 A2] [inst : IntoPersistently false A1 B] (h : P ∗ □ B ⊢ A2) : P ⊢ Q

theorem Iris.ProofMode.wand_intro_intuitionistic {PROP : Type u_1} [BI PROP] {P Q A1 A2 B : PROP} [FromWand Q A1 A2] [inst : IntoPersistently false A1 B] [or : Std.TCOr (BI.Affine A1) (BI.Absorbing A2)] (h : P ∗ □ B ⊢ A2) : P ⊢ Q

theorem Iris.ProofMode.imp_intro_spatial {PROP : Type u_1} [BI PROP] {P Q A1 A2 B : PROP} [FromImp Q A1 A2] [inst : FromAffinely B A1] [or : Std.TCOr (BI.Persistent A1) (BI.Intuitionistic P)] (h : P ∗ B ⊢ A2) : P ⊢ Q

theorem Iris.ProofMode.wand_intro_spatial {PROP : Type u_1} [BI PROP] {P Q A1 A2 : PROP} [FromWand Q A1 A2] (h : P ∗ A1 ⊢ A2) : P ⊢ Q

partial def Iris.ProofMode.iIntroCore {u : Lean.Level} {prop : Q(Type u)} (bi : Q(BI «$prop»)) {P : Q(«$prop»)} (hyps : Hyps bi P) (Q : Q(«$prop»)) (pats : List iCasesPat) (k : {P : Q(«$prop»)} → Hyps bi P → (Q : Q(«$prop»)) → Lean.MetaM Q(«$P» ⊢ «$Q»)) : Lean.MetaM Q(«$P» ⊢ «$Q»)

def Iris.ProofMode.tacticIintro__ : Lean.ParserDescr

Equations

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