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