On 2010-09-22 11:40, David Leduc wrote: > open import Relation.Nullary.Core The purpose of the Core modules is to break cycles in the module graph. They are not meant to be used directly. This is documented in the library's README. -- /NAD