proofIrr.agda:10,3-11,20
Datatypes in Prop must have at most one constructor when proof
irrelevance is enabled
when checking the definition of _\/_