On Mon, Apr 28, 2008 at 1:22 AM, Tristan Wibberley <tristan at wibberley.org> wrote: > > For example, boolean or: a proof object of "(a || b) istrue" is also a > proof object of "(b || a) istrue". Only in the case when the types are definitionally equal, i.e. only when both a and b are constructors, not in general. -- /NAD