∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (l : ℕ) (F : L.Functions l)
  (ts : Fin l → L.Term α) (f : ↥(FirstOrder.Language.func F ts).varFinset → β),
  (FirstOrder.Language.func F ts).restrictVar f =
    FirstOrder.Language.func F fun i => (ts i).restrictVar (f ∘ Set.inclusion ⋯)