intro t ht
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
⊢ ∀ (a : Finset (Sentence L)), ↑a ⊆ T → ∃ a_2, ∃ (h : ↑a_2 ⊆ T), ∀ a_3 ∈ a, A ⟨a_2, ⋯⟩ ⊧ₘ a_3
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
inst✝ : ∀ (t : FinSubtheory T), Nonempty (A t)
H : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
this : DecidableEq (Set (FinSubtheory T))
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ ∃ a, ∃ (h : ↑a ⊆ T), ∀ a_1 ∈ t, A ⟨a, ⋯⟩ ⊧ₘ a_1