On 2021-03-14 23:47, mechvel at scico.botik.ru wrote: > * I failed to separate the proof. I suggest that you try to mark the proof parts with @0, so that they are erased by the compiler: https://agda.readthedocs.io/en/latest/language/runtime-irrelevance.html -- /NAD