The Coq mailing list

["Flavio L. C. de Moura" <flaviomoura AT unb.br>]

Hello,

   This is probably a simple question, but I didn't manage to solve it...
   I have a binary predicate, say my_pred n t. The first argument is a 
natural and the second is an term of inductive type. In the induction 
step I get an expression of the form my_pred (n+1) t' where t' is 
simpler than t, and hence I can apply the induction hypothesis, but the 
induction hypothesis refers to the expression my_pred n t'. In a paper 
and pencil proof this step is trivial, but how can I instruct Coq to 
apply the induction hypothesis correctly?
Thank you in advance!

Best regards,

Flávio.