Realization of first-order terms and universally closed formulas

FirstOrder.Language.Term.realize_congr_varFinsetLeft says that a term over α ⊕ β has the same realization under two valuations of α that agree on the variables Term.varFinsetLeft it mentions. It is derived from Mathlib's Term.realize_restrictVarLeft', since Mathlib has no direct congruence lemma of this form.

FirstOrder.Language.Sentence.realize_alls characterizes satisfaction of the universal closure of a bounded formula with no free variables as realization at every tuple of bound variables.

theorem FirstOrder.Language.Term.realize_congr_varFinsetLeft {L : Language} {α : Type u_1} {β : Type u_2} {M : Type u_3} [L.Structure M] [DecidableEq α] {t : L.Term (α ⊕ β)} {v v' : α → M} (h : Set.EqOn v v' ↑t.varFinsetLeft) (xs : β → M) : realize (Sum.elim v xs) t = realize (Sum.elim v' xs) t

A term over α ⊕ β has the same realization under two valuations of α that agree on the variables Term.varFinsetLeft of α it mentions.

@[simp]

theorem FirstOrder.Language.Sentence.realize_alls {L : Language} {M : Type u_1} [L.Structure M] {n : ℕ} (φ : L.BoundedFormula Empty n) : M ⊨ φ.alls ↔ ∀ (a : Fin n → M), φ.Realize Empty.elim a

A universally closed sentence holds iff its body holds at every tuple.