[Agda] Q: Equational Reasoning

[Andrej Bauer]

On Wed, May 27, 2009 at 8:34 AM, Liang-Ting Chen
<xcycl at iis.sinica.edu.tw> wrote:
>
> Relation.Binary.PropositionalEquality.cong works for most case.
>

I am trying to wrap my brain around this. It would greatly help if
someone were kind enough to show how this is used to prove f(x,g(a)) =
f(x,g(b)) from a = b. and what if we used setoids and we only knew
that a and b are equivalent, and that f and g respect the
equivalences?

Thanks!

Andrej