intro i
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
⊢ ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
i : FinSubtheory T
⊢ ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i