theorem Iris.ProofMode.from_or_l {PROP : Type u_1} [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A1) : P ⊢ Q

def Iris.ProofMode.tacticIleft : Lean.ParserDescr

Equations

• Iris.ProofMode.tacticIleft = Lean.ParserDescr.node `Iris.ProofMode.tacticIleft 1024 (Lean.ParserDescr.nonReservedSymbol "ileft" false)

theorem Iris.ProofMode.from_or_r {PROP : Type u_1} [BI PROP] {P Q A1 A2 : PROP} [inst : FromOr Q A1 A2] (h1 : P ⊢ A2) : P ⊢ Q

def Iris.ProofMode.tacticIright : Lean.ParserDescr

Equations

• Iris.ProofMode.tacticIright = Lean.ParserDescr.node `Iris.ProofMode.tacticIright 1024 (Lean.ParserDescr.nonReservedSymbol "iright" false)