Can not be defined as an axiom that different constructors create different terms? To prove 0<>1 without using bottom. To be consistent. Regards, Patricia Peratto -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200201/53285385/attachment.html>