[Agda] Q: Equational Reasoning

[Andrej Bauer]

Hi,

this might be a good opportunity to ask.  How does Agda deal with
equational reasoning in subterms? It's one thing to say "use
commutativity to prove that a * b equals b * a", but it's a different
game when we say "use commutativity to prove that f(x, g(a * b)) =
f(x, g(b* a))"?

A more basic question is how to explain to agda that the fact a=b can
be used to replace a by b in an expression.

I am asking because I think Agda is very c00l, but I do not see (yet)
whether it's suitable for developing large swaths of mathematics. Any
opinions about that? What would it take to prove the fundamental
theorem of calculus, for example?

Andrej