rcases hp with (⟨π, hπ, rfl⟩ | rfl)
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
h : (Evalfm s.Dom fun x_1 => x) p
hp : (∃ a ∈ b.antecedent, ~Rew.emb.hom a = p) ∨ p = Rew.emb.hom σ
⊢ 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 π)
⊢ s ⊧ σ

case intro.intro.intro.inr
L : Language
T : Set (Sentence L)
σ : Sentence L
b : T ⊢ σ
s : Struc L
hT : s ∈ Semantics.models (Struc L) T
x : s.Dom
h : (Evalfm s.Dom fun x_1 => x) (Rew.emb.hom σ)
⊢ s ⊧ σ