no goals
L : Language
L' : Language
M : Type w
N : Type ?u.782402
P : Type ?u.782405
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
T : Theory L
⊢ M ⊨ infiniteTheory L ↔ Infinite M
simp [infiniteTheory, infinite_iff, aleph0_le]