The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi Thomas,

You're applying the induction hypothesis too late. If you do

Lemma preservationOfSubstitution: forall (G:context) (x:termType) (t  
s:term)
   (T S:type),
   typing ((x, S) :: G) t T ->
   typing G s S ->
   typing G (termSubst x s t) T.
Proof.
  induction t.

instead of doing itnros first, you'll find that the T in the induction  
hypothesis is universally quantified.

Generally, if you do induction over something, you should avoid  
introducing unnecessary other variables first as your induction  
hypothesis might not be useable.

Hope that helps,

Edsko