∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : L.Term α) → (↥x.varFinset → β) → Sort u_4) (l : ℕ) (F : L.Functions l) (ts : Fin l → L.Term α)
  (f : ↥(FirstOrder.Language.func F ts).varFinset → β)
  (h_1 : (a : α) → (f : ↥(FirstOrder.Language.var a).varFinset → β) → motive (FirstOrder.Language.var a) f)
  (h_2 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term α) →
          (f : ↥(FirstOrder.Language.func F ts).varFinset → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.func F ts, f with
    | FirstOrder.Language.var a, f => h_1 a f
    | FirstOrder.Language.func F ts, f => h_2 l F ts f) =
    h_2 l F ts f