The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

For instance, does this mean
that the tactic "rewrite" can now be used under a lambda-abstraction? That
would be tremendously useful.

Nothing new under the sun on this part. You can rewrite under lambda abstraction as long as abstracting out the subterm under consideration doesn't affect the _expression_'s type. This, in particular excludes subterms with bound variables. (e.g. you won't be able to prove (fun x=>x)=(fun x=>tt). The bottom line is that eta-expansion at the level of conversion is weaker than propositional extensionality.

So, mostly, it makes unification more potent (which is not without pitfalls).


Arnaud