The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

franck.barbier AT franckbarbier.com
 wrote:
> I become quite mad on the second proof... I guess there are two solutions. The
> proof is "too much trivial" or artificially complicated, even not proovable ?
>
> Inductive X : Type := God | cons : X ->  X.
>    

This type is isomorphic to the natural numbers [nat], and your theorem 
is pretty easy to reduce to a set of facts about arithmetic, all of 
which can be proven by the [omega] tactic.  My hint is to write a 
function to translate [X] to [nat] and then characterize the action of 
your [ancestor] function in terms of standard arithmetic operations.