Why does substitution terminate?
Derek Elkins' comment solved my problem! Here's the solution I came up with:

We create a seperate renaming function rename: Term -&gt; nat -&gt; nat -&gt; Term, which assumes that the name to rename with is fresh. This makes it trivially terminating.

Fixpoint rename (t:Term) (x y : nat): Term :=
  match t with
  | TVar z =&gt;
    if beq_nat y z then TVar x
    else TVar z
  | TApp t1 t2 =&gt;
    TApp (rename t1 x y) (rename t2 x y)
  | TAbs z t =&gt;
    if beq_nat y z then
      TAbs z t
    else
      TAbs z (rename t x y)
  end.


we then define a (somewhat arbitrary) measure of a term:

Fixpoint size (t:Term): nat :=
  match t with
    TVar _ =&gt; 1
  | TApp t1 t2 =&gt; size t1 + size t2
  | TAbs x t =&gt; 2 + size t
  end.


and we can easily prove that renaming preserves this measure:

Lemma rename_preserves_size:
  forall t x y,
    size t = size (rename t x y).


this lemma is used in the final case of substitition in order to prove that the term rename t y' y has the same size as t and thus the call substitute (rename t y' y) t2 x happens on a strictly smaller term.

Now all I need to prove that this is correct.