> Is there a way to tell Agda not to unfold these definitions in goals? Have you tried using the abstract keyword? I seem to remember that it can be used prevent the definition being unfolded (but I can't seem to find any documentation). Wouter