Commit 2022-09-19 20:38 b3951c65

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.