+ <para>
+ This tactic is under development.
+ It simplifies the current context by removing
+ <command>H</command> using the following methods:
+ forward application of a suitable simplification theorem (chosen
+ automatically) of which the type of <command>H</command> is a
+ premise, decomposition, rewriting.
+ </para>