simp [hq]
L : Language
Δ : List (SyntacticSemiformula L 0)
p : Semiformula L ℕ (0 + 1)
d : Derivation ((Rew.hom Rew.free) p :: shifts Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
q : SyntacticSemiformula L 0
hq : q ∈ Δ
hhq : (Evalfm M ε) q
⊢ q ∈ (∀' p) :: Δ
no goals