simp [hn]
L : Language
Δ : List (SyntacticFormula L)
p : SyntacticFormula L
d : Derivation (p :: Δ)
dn : Derivation (~p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
h : (Evalfm M ε) p
q : SyntacticFormula L
hn : q ∈ Δ
hq : (Evalfm M ε) q
⊢ q ∈ Δ
no goals