assume id : sterm

The conclusion of the sequent to prove must be a universal quantification.

It applies the right introduction rule for the universal quantifier, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the quantifier).

It opens a new sequent to prove the quantified subformula adding x : T to the hypotheses.