transitivity sterm

The conclusion of the current proof must be an equality.

It closes the current sequent by transitivity of the equality.

It opens two new sequents l=t and t=r where l and r are the left and right hand side of the equality in the conclusion of the current sequent to prove.