[Agda] Examples of tacticts via reflection

[Gyesik Lee]

> P.S. I suspect many users of Coq come to the Agda wiki to see what it
> is about. It would be great if there were a page for them, explaining
> the similarities and the differences.

At AIM9, when I had the first contact with Agda, I found Ulf's
tutorial very instructive.

"Dependently Typed Programming in Agda"

I tried to make some comparison with Coq and made some comments.
I should have posted my comments to Agda wiki, sorry for this.
I'll do it soon.

Gyesik