∀ {L : FirstOrder.Language} {α : Type u'} (a : α) (l : List (α ⊕ (i : ℕ) × L.Functions i)),
  FirstOrder.Language.Term.listDecode (Sum.inl a :: l) =
    FirstOrder.Language.var a :: FirstOrder.Language.Term.listDecode l