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). H₀ ... H_n are passed to the tactics fwd invokes, as names for the premise they introduce.

The ones opened by the tactics fwd invokes.