Theorem: LO.System.Context.not_mem_empty (Logic/Logic/HilbertStyle/Context.lean)

State before:
F : Type u_1
inst✝² : LogicalConnective F
inst✝¹ : DecidableEq F
S : Type u_2
inst✝ : System F S
𝓢 : S
p : F
⊢ p ∉ ∅
Tactic:
simp [EmptyCollection.emptyCollection, Set.mem_def]
State after:
no goals