theorem LO.FirstOrder.ModelsTheory.of_provably_subtheory {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) : T ≼ U → M ⊧ₘ* U → M ⊧ₘ* T

theorem LO.FirstOrder.ModelsTheory.of_provably_subtheory' {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) [T ≼ U] [M ⊧ₘ* U] : M ⊧ₘ* T

theorem LO.FirstOrder.ModelsTheory.of_add_left {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) [M ⊧ₘ* T + U] : M ⊧ₘ* T

theorem LO.FirstOrder.ModelsTheory.of_add_right {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) [M ⊧ₘ* T + U] : M ⊧ₘ* U

theorem LO.FirstOrder.ModelsTheory.of_add_left_left {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) (V : LO.FirstOrder.Theory L) [M ⊧ₘ* T + U + V] : M ⊧ₘ* T

theorem LO.FirstOrder.ModelsTheory.of_add_left_right {L : LO.FirstOrder.Language} (M : Type w) [Nonempty M] [LO.FirstOrder.Structure L M] (T : LO.FirstOrder.Theory L) (U : LO.FirstOrder.Theory L) (V : LO.FirstOrder.Theory L) [M ⊧ₘ* T + U + V] : M ⊧ₘ* U

theorem LO.FirstOrder.completeness_iff_with_eq {L : LO.FirstOrder.Language} [L.Eq] {T : LO.FirstOrder.Theory L} {σ : LO.FirstOrder.Sentence L} : T⁼ ⊨ σ ↔ T⁼ ⊢! σ