[Agda] Status of Prop

[Nils Anders Danielsson]

On Fri, Sep 5, 2008 at 14:39, Andres Loeh <andres at cs.uu.nl> wrote:
>
> I was mainly thinking about Agda's ability to infer the
> one inhabitant of the record type, but not the one element
> of the datatype.

Well, this follows from η.

-- 
/NAD