no goals
L : Language
κ : Cardinal
T✝ : Theory L
T : Theory Language.empty
M N : Theory.ModelType T
hM : (#↑M) = κ
hN : (#↑N) = κ
⊢ Nonempty (↑M ≃[Language.empty] ↑N)
rw [empty.nonempty_equiv_iff, hM, hN]