DEFINITION iso_ind()
TYPE =
       ∀P:T→T→Prop
         .∀n:nat.∀n1:nat.(P (TSort n) (TSort n1))
           →(∀n:nat.∀n1:nat.(P (TLRef n) (TLRef n1))
                →(∀t:T.∀t1:T.∀t2:T.∀t3:T.∀k:K.(P (THead k t t2) (THead k t1 t3)))→∀t:T.∀t1:T.(iso t t1)→(P t t1))
BODY =
        assume P: T→T→Prop
        suppose H: ∀n:nat.∀n1:nat.(P (TSort n) (TSort n1))
        suppose H1: ∀n:nat.∀n1:nat.(P (TLRef n) (TLRef n1))
        suppose H2: ∀t:T.∀t1:T.∀t2:T.∀t3:T.∀k:K.(P (THead k t t2) (THead k t1 t3))
        assume t: T
        assume t1: T
        suppose H3: iso t t1
          by cases on H3 we prove P t t1
             case iso_sort n:nat n1:nat ⇒
                the thesis becomes P (TSort n) (TSort n1)
                by (H . .)
P (TSort n) (TSort n1)
             case iso_lref n:nat n1:nat ⇒
                the thesis becomes P (TLRef n) (TLRef n1)
                by (H1 . .)
P (TLRef n) (TLRef n1)
             case iso_head t2:T t3:T t4:T t5:T k:K ⇒
                the thesis becomes P (THead k t2 t4) (THead k t3 t5)
                by (H2 . . . . .)
P (THead k t2 t4) (THead k t3 t5)
          we proved P t t1
       we proved 
          ∀P:T→T→Prop
            .∀n:nat.∀n1:nat.(P (TSort n) (TSort n1))
              →(∀n:nat.∀n1:nat.(P (TLRef n) (TLRef n1))
                   →(∀t:T.∀t1:T.∀t2:T.∀t3:T.∀k:K.(P (THead k t t2) (THead k t1 t3)))→∀t:T.∀t1:T.(iso t t1)→(P t t1))