rcases Derivation.sound b.derivation s.Dom (fun _ ↦ x) with ⟨p, hp, h⟩
case intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
⊢ s ⊧ σ
case intro.intro.intro
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
p : SyntacticFormula L
hp : p ∈ List.map (⇑Rew.emb.hom) (List.map (fun x => ~x) b.antecedent ++ [σ])
h : (Evalfm s.Dom fun x_1 => x) p
⊢ s ⊧ σ