no goals
L : Language
L' : Language
M : Type w
N : Type ?u.330070
P : Type ?u.330073
inst✝⁴ : Structure L M
inst✝³ : Structure L N
inst✝² : Structure L P
α : Type u'
β : Type v'
n : ℕ
T✝ : Theory L
inst✝¹ : Structure L' M
φ : L →ᴸ L'
inst✝ : IsExpansionOn φ M
T : Theory L
⊢ M ⊨ onTheory φ T ↔ M ⊨ T
simp [Theory.model_iff, LHom.onTheory]