Why does substitution terminate? I'm formalizing some properties of lambda calculus in Coq and I have some problems proving termination of substitution. My terms are defined as:

Inductive Term :=
  TVar: nat -&gt; Term
| TAbs: nat -&gt; Term -&gt; Term
| TApp: Term -&gt; Term -&gt; Term.


and I have a way of generating fresh variables using a function

fresh: Term -&gt; nat


satisfying:

Lemma fresh_is_fresh:
  forall t,
    ~ FV t (fresh t).


and similarly a function fresh2: Term -&gt; Term -&gt; nat for obtaining a fresh identifier wrt. two terms.

I now want to define a standard notion of capture avoiding substitution:

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


Obviously, Coq cannot see that this definition is terminating, so I need to provide a custom measure, so that the code is something like the following:

Program Fixpoint substitute (t1:Term) (t2:Term) (x:nat) {measure ???}: Term :=
  match t1 with
  | TVar y =&gt;
    if beq_nat x y then t2 else TVar y
  | TApp t11 t12 =&gt;
    TApp (substitute t11 t2 x) (substitute t12 t2 x)
  | TAbs y t =&gt;
    if beq_nat x y then
      TAbs x t
    else TAbs (fresh2 t t1) (substitute (substitute t (TVar y) (fresh2 t t1)) t2 x)
  end.


Now my question is: What is the correct measure to use here? And how I do use it to prove the obligations which arise using this measure?
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.