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 =
Show proof