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
⊢ (∀ (a : M), (Evalm M ![a] ε) p) ∨ ∃ q ∈ Δ, (Evalfm M ε) q
no goals