have : (∀ a : M, Evalm M ![a] ε p) ∨ ∃ q ∈ Δ, Evalfm M ε q := by
  simpa[shifts, shiftEmb, Matrix.vecConsLast_vecEmpty, forall_or_right]
    using fun a : M => sound d M (a :>ₙ ε)
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
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1
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
this : (∀ (a : M), (Evalm M ![a] ε) p) ∨ ∃ q ∈ Δ, (Evalfm M ε) q
⊢ ∃ p_1 ∈ (∀' p) :: Δ, (Evalfm M ε) p_1