letin

letin x ≝ t

Synopsis:

letin id sterm

Pre-conditions:

None.

Action:

It adds to the context of the current sequent to prove a new definition x ≝ t.

New sequents to prove:

None.