DEFINITION csuba_refl()
TYPE =
       ∀g:G.∀c:C.(csuba g c c)
BODY =
        assume g: G
        assume c: C
          we proceed by induction on c to prove csuba g c c
             case CSort : n:nat ⇒
                the thesis becomes csuba g (CSort n) (CSort n)
                   by (csuba_sort . .)
csuba g (CSort n) (CSort n)
             case CHead : c0:C k:K t:T ⇒
                the thesis becomes csuba g (CHead c0 k t) (CHead c0 k t)
                (H) by induction hypothesis we know csuba g c0 c0
                   by (csuba_head . . . H . .)
csuba g (CHead c0 k t) (CHead c0 k t)
          we proved csuba g c c
       we proved ∀g:G.∀c:C.(csuba g c c)