lapply [linear] [depth=nat] sterm [to sterm [,sterm…] ] [as id]

t must have at least d independent premises and n must not be greater than d.

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₁, ..., 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₁, ..., t_n are (applications of) premises in the current context, they are cleared.

The ones opened by the tactics lapply invokes.