Matita Home

`transitivity t`

- Synopsis:
**transitivity***sterm*- Pre-conditions:
The conclusion of the current proof must be an equality.

- Action:
It closes the current sequent by transitivity of the equality.

- New sequents to prove:
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.