Theorem: LO.System.Context.by_axm! (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
inst✝ : Minimal 𝓢
p : F
Γ : Set F
h : p ∈ Γ
⊢ p ∈ Collection.set { ctx := Γ }
Tactic:
simpa
State after:
no goals