DEFINITION iso_refl()
TYPE =
       ∀t:T.(iso t t)
BODY =
       assume t: T
          we proceed by induction on t to prove iso t t
             case TSort : n:nat ⇒
                the thesis becomes iso (TSort n) (TSort n)
                   by (iso_sort . .)
iso (TSort n) (TSort n)
             case TLRef : n:nat ⇒
                the thesis becomes iso (TLRef n) (TLRef n)
                   by (iso_lref . .)
iso (TLRef n) (TLRef n)
             case THead : k:K t0:T t1:T ⇒
                the thesis becomes iso (THead k t0 t1) (THead k t0 t1)
                () by induction hypothesis we know iso t0 t0
                () by induction hypothesis we know iso t1 t1
                   by (iso_head . . . . .)
iso (THead k t0 t1) (THead k t0 t1)
          we proved iso t t
       we proved ∀t:T.(iso t t)