theorem Iris.ProofMode.exists_intro' {PROP : Type u_1} {α : Sort u_2} [BI PROP] {Φ : α → PROP} {P Q : PROP} [inst : FromExists Q Φ] (a : α) (h : P ⊢ Φ a) : P ⊢ Q

def Iris.ProofMode.tacticIexists_ : Lean.ParserDescr

Equations

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