∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ)
  (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β),
  FirstOrder.Language.BoundedFormula.falsum.restrictFreeVar _f = FirstOrder.Language.BoundedFormula.falsum