no goals
L : Language
M : Type u_3
N : Type ?u.401025
P : Type ?u.401028
Q : Type ?u.401031
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
S : ElementarySubstructure L M
T : Theory L
⊢ { x // x ∈ S } ⊨ T ↔ M ⊨ T
simp only [Theory.model_iff, realize_sentence]