INDUCTIVE DEFINITION iso () [ ]
OF ARITY T→T→Prop
BUILT FROM:
     iso_sort: ∀n1:nat.∀n2:nat.(iso (TSort n1) (TSort n2))
   | iso_lref: ∀i1:nat.∀i2:nat.(iso (TLRef i1) (TLRef i2))
   | iso_head: ∀v1:T.∀v2:T.∀t1:T.∀t2:T.∀k:K.(iso (THead k v1 t1) (THead k v2 t2))