The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

frank maltman wrote:
> However, I'm now stuck proving the first case that does terminate:
>
> --8<--
>
> Lemma pred_numeric_not_stuck : forall (t : term),
>    numeric t = true ->  error (one_step (Term_Pred t)) = false.
> Proof.
>    intros t H.
>    induction t.
> [...]
>
> I have 'error (one_step (Term_Pred t)) = false' as an induction hypothesis 
> but am
> unable to prove 'error (one_step (Term_Pred (Term_Pred t))) = false' with it.
>    

I don't think your question is really about Coq.  This proof strategy 
fails on paper, too.

Have you convinced yourself that you have a valid informal proof?  
That's usually a good first step before formalizing.