`TRANS : thm -> thm -> thm`

SYNOPSIS
Uses transitivity of equality on two equational theorems.

DESCRIPTION
When applied to a theorem A1 |- t1 = t2 and a theorem A2 |- t2' = t3, where t2 and t2' are alpha-equivalent (in particular, where they are identical), the inference rule TRANS returns the theorem A1 u A2 |- t1 = t3.
```    A1 |- t1 = t2   A2 |- t2' = t3
--------------------------------  TRANS
A1 u A2 |- t1 = t3
```

FAILURE CONDITIONS
Fails unless the theorems are equational, with the right side of the first being the same as the left side of the second, up to alpha-equivalence.

EXAMPLE
The following shows identical uses of TRANS, one on Boolean equations (shown as <=>) and one on numerical equations.
```  # let t1 = ASSUME `a:bool = b` and t2 = ASSUME `b:bool = c`;;
val t1 : thm = a <=> b |- a <=> b
val t2 : thm = b <=> c |- b <=> c
# TRANS t1 t2;;
val it : thm = a <=> b, b <=> c |- a <=> c

# let t1 = ASSUME `x:num = 1` and t2 = num_CONV `1`;;
val t1 : thm = x = 1 |- x = 1
val t2 : thm = |- 1 = SUC 0
# TRANS t1 t2;;
val it : thm = x = 1 |- x = SUC 0
```