Matita Home

`fwd H as H`

_{0} ... H_{n}

- Synopsis:
- Pre-conditions:
The type of

**H**must be the premise of a forward simplification theorem.- Action:
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**are passed to the tactics_{0}... H_{n}**fwd**invokes, as names for the premise they introduce.- New sequents to prove:
The ones opened by the tactics

**fwd**invokes.