lapply linear depth=d t to t1, ..., tn as H


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

New sequents to prove:

The ones opened by the tactics lapply invokes.