have : ¬s ⊧ π := by simpa using h
case intro.intro.intro.inl.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
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this : s ⊧ π
⊢ s ⊧ σ
case intro.intro.intro.inl.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
π : Sentence L
hπ : π ∈ b.antecedent
h : (Evalfm s.Dom fun x_1 => x) (~Rew.emb.hom π)
this✝ : s ⊧ π
this : ¬s ⊧ π
⊢ s ⊧ σ