simpa[eval_substs, Matrix.constant_eq_singleton] using sound d M ε
L : Language
Δ : List (SyntacticFormula L)
p : Semiformula L ℕ (Nat.succ 0)
t : Semiterm L ℕ 0
d : Derivation ([→ t].hom p :: Δ)
M : Type u_1
s : Structure L M
ε : ℕ → M
⊢ (Evalm M ![Semiterm.valm M ![] ε t] ε) p ∨ ∃ p ∈ Δ, (Evalfm M ε) p
no goals