[Agda] rewriting product types vs. single ctor data/record types

[Nils Anders Danielsson]

On 2013-08-25 19:45, Jonathan Leivent wrote:
> Is there some way to rewrite "into" the fields of a data/record type
> that appears as a goal, to achieve the same effect as rewriting would
> on a very similar product type?

If you change the fields' types, then you may end up with something that
is no longer an instance of the record type.

-- 
/NAD