feat(model_theory/*): Lemmas about satisfiability (#16546)
Proves that applying an injective language map to a theory does not change its satisfiability (`first_order.language.Theory.is_satisfiable_of_is_satisfiable_on_Theory`)
Proves that a union of theories is satisfiable iff any finite union of the theories is (`first_order.language.Theory.is_satisfiable_Union_iff_is_satisfiable_Union_finset`)
Proves a few other minor satisfiability and language map lemmas.
Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>
