DEFINITION iso_trans()
TYPE =
       ∀t1:T.∀t2:T.(iso t1 t2)→∀t3:T.(iso t2 t3)→(iso t1 t3)
BODY =
        assume t1: T
        assume t2: T
        suppose H: iso t1 t2
          we proceed by induction on H to prove ∀t3:T.(iso t2 t3)→(iso t1 t3)
             case iso_sort : n1:nat n2:nat ⇒
                the thesis becomes ∀t3:T.∀H0:(iso (TSort n2) t3).(iso (TSort n1) t3)
                    assume t3: T
                    suppose H0: iso (TSort n2) t3
                      (H_x) 
                         by (iso_gen_sort . . H0)
ex nat λn2:nat.eq T t3 (TSort n2)
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove iso (TSort n1) t3
                         case ex_intro : x:nat H2:eq T t3 (TSort x) ⇒
                            the thesis becomes iso (TSort n1) t3
                               by (iso_sort . .)
                               we proved iso (TSort n1) (TSort x)
                               by (eq_ind_r . . . previous . H2)
iso (TSort n1) t3
                      we proved iso (TSort n1) t3
∀t3:T.∀H0:(iso (TSort n2) t3).(iso (TSort n1) t3)
             case iso_lref : i1:nat i2:nat ⇒
                the thesis becomes ∀t3:T.∀H0:(iso (TLRef i2) t3).(iso (TLRef i1) t3)
                    assume t3: T
                    suppose H0: iso (TLRef i2) t3
                      (H_x) 
                         by (iso_gen_lref . . H0)
ex nat λn2:nat.eq T t3 (TLRef n2)
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove iso (TLRef i1) t3
                         case ex_intro : x:nat H2:eq T t3 (TLRef x) ⇒
                            the thesis becomes iso (TLRef i1) t3
                               by (iso_lref . .)
                               we proved iso (TLRef i1) (TLRef x)
                               by (eq_ind_r . . . previous . H2)
iso (TLRef i1) t3
                      we proved iso (TLRef i1) t3
∀t3:T.∀H0:(iso (TLRef i2) t3).(iso (TLRef i1) t3)
             case iso_head : v1:T v2:T t3:T t4:T k:K ⇒
                the thesis becomes ∀t5:T.∀H0:(iso (THead k v2 t4) t5).(iso (THead k v1 t3) t5)
                    assume t5: T
                    suppose H0: iso (THead k v2 t4) t5
                      (H_x) 
                         by (iso_gen_head . . . . H0)
ex_2 T T λv2:T.λt2:T.eq T t5 (THead k v2 t2)
                      end of H_x
                      (H1) consider H_x
                      we proceed by induction on H1 to prove iso (THead k v1 t3) t5
                         case ex_2_intro : x0:T x1:T H2:eq T t5 (THead k x0 x1) ⇒
                            the thesis becomes iso (THead k v1 t3) t5
                               by (iso_head . . . . .)
                               we proved iso (THead k v1 t3) (THead k x0 x1)
                               by (eq_ind_r . . . previous . H2)
iso (THead k v1 t3) t5
                      we proved iso (THead k v1 t3) t5
∀t5:T.∀H0:(iso (THead k v2 t4) t5).(iso (THead k v1 t3) t5)
          we proved ∀t3:T.(iso t2 t3)→(iso t1 t3)
       we proved ∀t1:T.∀t2:T.(iso t1 t2)→∀t3:T.(iso t2 t3)→(iso t1 t3)