choose A si s hA using this
case mpr
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
this : ∀ (i : FinSubtheory T), ∃ M, ∃ (x : Nonempty M), ∃ x_1, M ⊧ₘ* ↑↑i
⊢ Satisfiable T
case mpr
L : Language
T : Theory L
A✝ : FinSubtheory T → Type u
s✝ : (i : FinSubtheory T) → Structure L (A✝ i)
h : ∀ (i : FinSubtheory T), Satisfiable ↑↑i
A : FinSubtheory T → Type u
si : ∀ (i : FinSubtheory T), Nonempty (A i)
s : (i : FinSubtheory T) → Structure L (A i)
hA : ∀ (i : FinSubtheory T), A i ⊧ₘ* ↑↑i
⊢ Satisfiable T