errors/PropMustBeSingleton.agda:6,3-7,21
Datatypes in Prop must have at most one constructor when proof
irrelevance is enabled
when checking the definition of _\/_