let x := T
let id = term
None
It adds a new local definition x := T to the context of the sequent to prove.
None.
Matita Home