∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {n m : ℕ} {φ : L.BoundedFormula α n}
  {v : α → M} {xs : Fin (n + 1) → M},
  m ≤ n →
    ((FirstOrder.Language.BoundedFormula.liftAt 1 m φ).Realize v xs ↔
      φ.Realize v (xs ∘ fun i => if ↑i < m then i.castSucc else i.succ))