The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 7 Jun 2008, 
roconnor AT theorem.ca
 wrote:

> Right. I thought about this an hour after I sent my email.  The problem is 
> that we really want the lemma forall x:Stream, x=cons x to hold because 
> exactly the same proof holds for
>
> Inductive Stream' : Type := cons' : Stream' -> Stream'.
>
> I'd wager that (forall x:Stream, x=cons x) ought to hold for any fixed point 
> of Identity, whether it is greatest, least, or otherwise.

I'm wrong about this too.  It is (forall x:Stream, x=out x) that holds for 
any fixed point of Identity.  Prehaps it is okay then for (cons oneones) 
to no be convertable with oneones.  I guess I should take more time to 
think before replying.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''