no goals
L : Language
α : Type w
M : Type w'
n : ℕ
inst✝³ : IsOrdered L
inst✝² : Structure L M
inst✝¹ : LE M
inst✝ : OrderedStructure L M
t₁ t₂ : Term L (α ⊕ Fin n)
v : α → M
xs : Fin n → M
⊢ BoundedFormula.Realize (le t₁ t₂) v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂
simp [Term.le]