19.3 Is it automatic ?

Yes, building the variables map and doing the substitution after normalizing is automaticaly done by the tactic. So you can just forget this paragraph and use the tactic according to your intuition.

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.8.2.html at 8/10/98