∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_3} (motive : L.Term (α ⊕ β) → Sort u_5) (_i : β)
  (h_1 : (i : α) → motive (FirstOrder.Language.var (Sum.inl i)))
  (h_2 : (_i : β) → motive (FirstOrder.Language.var (Sum.inr _i)))
  (h_3 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term (α ⊕ β)) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.var (Sum.inr _i) with
    | FirstOrder.Language.var (Sum.inl i) => h_1 i
    | FirstOrder.Language.var (Sum.inr _i) => h_2 _i
    | FirstOrder.Language.func _f ts => h_3 l _f ts) =
    h_2 _i