∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (k : α)
  (h_1 : (k : α) → motive (FirstOrder.Language.var k))
  (h_2 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var k with
    | FirstOrder.Language.var k => h_1 k
    | FirstOrder.Language.func f ts => h_2 l f ts) =
    h_1 k