simpa using h
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 ⊧ σ
no goals