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