no goals
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.909458
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
h : M ≅[L] N
⊢ M ⊨ T ↔ N ⊨ T
rw [Theory.model_iff_subset_completeTheory, Theory.model_iff_subset_completeTheory,
  h.completeTheory_eq]