no goals
L : Language
M : Type u_3
N : Type u_4
P : Type ?u.262800
Q : Type ?u.262803
inst✝³ : Structure L M
inst✝² : Structure L N
inst✝¹ : Structure L P
inst✝ : Structure L Q
f : M ↪ₑ[L] N
T : Theory L
⊢ M ⊨ T ↔ N ⊨ T
simp only [Theory.model_iff, f.map_sentence]