theorem Iris.ProofMode.exfalso {PROP : Type u_1} [BI PROP] {P Q : PROP} (h : P ⊢ False) : P ⊢ Q

def Iris.ProofMode.tacticIexfalso : Lean.ParserDescr

Equations

• Iris.ProofMode.tacticIexfalso = Lean.ParserDescr.node `Iris.ProofMode.tacticIexfalso 1024 (Lean.ParserDescr.nonReservedSymbol "iexfalso" false)