assume id : sterm

The conclusion of the current proof must be ∀x:T.P or T→P where T is a data type (i.e. T has type Set or Type).

It adds to the context of the current sequent to prove a new declaration x : T . The new conclusion becomes P.

None.