rintro h ⟨t, ht⟩
case mp
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
⊢ Satisfiable T → ∀ (i : FinSubtheory T), Satisfiable ↑↑i
case mp.mk
L : Language
T : Theory L
A : FinSubtheory T → Type u
s : (i : FinSubtheory T) → Structure L (A i)
h : Satisfiable T
t : Finset (Sentence L)
ht : ↑t ⊆ T
⊢ Satisfiable ↑↑⟨t, ht⟩