∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} {n : ℕ} (g : α → β ⊕ Fin n) {k : ℕ} (φ : L.BoundedFormula α k),
  FirstOrder.Language.BoundedFormula.relabel g φ.not = (FirstOrder.Language.BoundedFormula.relabel g φ).not