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

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

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

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

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

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

theorem LO.FirstOrder.EQ.provOf {L : Language} [L.Eq] {T : Theory L} [𝐄𝐐 ≼ T] (φ : SyntacticFormula L) (H : ∀ (M : Type (max u w)) [inst : Nonempty M] [inst_1 : Structure L M] [inst_2 : Structure.Eq L M] [inst_3 : M ⊧ₘ* T], M ⊧ₘ φ) : T ⊨ φ