The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Edward Z. Yang wrote:
> Excerpts from Adam Chlipala's message of Thu Nov 03 16:27:13 -0400 2011:
>   
> > This is a common issue that is usually solved by proving (inductively) 
> > lemmas with extra variables and equalities.  In your example here, you 
> > could also prove [forall x y, cop' x y -> cop x y] and then derive 
> > [cop'_op] as an easy corollary of [cop_op].
> >     
>
> OK, I could see how that works.  But barring a major benefit I would
> probably not bother with cop' then, and always write out my equalities
> in the long form...
>   

That is one reasonable choice.  I find the equality-free inductive type 
definitions easier to read, which makes it easier to convince yourself 
in the end that you proved the right theorem.  For that reason, I favor 
extra work with lemmas and equalities.