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.EQ.provOf {L : LO.FirstOrder.Language} [L.Eq] {T : LO.FirstOrder.Theory L} [𝐄𝐐 ≼ T] (p : LO.FirstOrder.SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : LO.FirstOrder.Structure L M] [inst_2 : LO.FirstOrder.Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ p) : T ⊨ p