The Coq mailing list

[Nikhil Swamy <nswamy AT microsoft.com>]

> You could also define a size function for the derivations and do well-
> founded induction on it, then you
> can apply your transitivity induction hypothesis on smaller
> derivations. One has to take care that
> size information is propagated in the generation/inversion lemmas in
> this case. I tried both the counters
> and the size function in one of my formalizations and in the end I
> think I prefer the later, which is
> also common in pencil-and-paper proofs.
> 
> Hope this helps,
> -- Matthieu

Thanks for this tip Matthieu. I'll give this approach a shot at some point 
and report back. 
-Nik