On 2011-12-16 12:39, Conor McBride wrote: > PS In the presence of equality on sets, where coercion between > provably equal sets is definable, it is possible to replace very > many type errors by irredeemable metavariables, turning brown to > yellow. What are you referring to here? -- /NAD