The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Robin Green wrote:
> >  [With Program] The program you write will in general not be the
> > Gallina term that you end up with, and it's that Gallina term that
> > you'd need to prove things about.
> >     
>
> True, but so what? You can still see the term, but there's no need to
> put it in the source file.
>   

Terms with coercions are _much_ harder to reason about than terms without.