{L : FirstOrder.Language} →
  {α : Type u_3} →
    (motive : L.Term α → Sort u_4) →
      (x : L.Term α) →
        ((i : α) → motive (FirstOrder.Language.var i)) →
          ((l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)) → motive x