[Agda] Making ≡ proofs more manageable

[Helmut Grohne]

On Mon, Jan 13, 2014 at 08:30:20AM +0000, Mateusz Kowalczyk wrote:
> Is there any way to make proofs of such form more manageable? Any
> tricks? It's fairly clear that the meat of the proof is just down to
> showing a few bits inside of this rather large goal type. Perhaps
> there's a method to get those in an easier manner rather than retyping
> the whole thing at each step of the proof.

Occasionally I find the unnormalized (C-u C-c C-,) goal types
insightful. Of course this works badly if you excessively use lambda
expressions. So you'd need to start naming those expressions to use this
tool effectively.

Furthermore, it seems that the outermost bits of your equality type are
equal. Maybe a custom cong lifting some kind of pointwise equality on
the contained functions to a Parser equality can cut down in length?

Helmut