fwd H as H0 ... Hn


fwd id [as id [id]…]


The type of H must be the premise of a forward simplification theorem.


This tactic is under development. It simplifies the current context by removing H using the following methods: forward application (by lapply) of a suitable simplification theorem, chosen automatically, of which the type of H is a premise, decomposition (by decompose), rewriting (by rewrite). H0 ... Hn are passed to the tactics fwd invokes, as names for the premise they introduce.

New sequents to prove:

The ones opened by the tactics fwd invokes.