Matita Home

```
lapply linear depth=d t
to t
```

_{1}, ..., t_{n} as H

- Synopsis:
**lapply**[**linear**] [**depth=***nat*]*sterm*[**to***sterm*[**,***sterm*…] ] [**as***id*]- Pre-conditions:
**t**must have at least**d**independent premises and**n**must not be greater than**d**.- Action:
Invokes

**letin H ≝ (t ? ... ?)**with enough**?**'s to reach the**d**-th independent premise of**t**(**d**is maximum if unspecified). Then istantiates (by**apply**) with t_{1}, ..., t_{n}the**?**'s corresponding to the first**n**independent premises of**t**. Usually the other**?**'s preceding the**n**-th independent premise of**t**are istantiated as a consequence. If the**linear**flag is specified and if**t, t**are (applications of) premises in the current context, they are_{1}, ..., t_{n}**clear**ed.- New sequents to prove:
The ones opened by the tactics

**lapply**invokes.