∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {m n : ℕ} (h : m = n) {h' : m ≤ n}
  {φ : L.BoundedFormula α m} {v : α → M} {xs : Fin n → M},
  (FirstOrder.Language.BoundedFormula.castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)