DEFINITION iso_trans()
TYPE =
       ∀t1:T.∀t2:T.(iso t1 t2)→∀t3:T.(iso t2 t3)→(iso t1 t3)
BODY =
Show proof