DEFINITION csubv_refl()
TYPE =
       ∀c:C.(csubv c c)
BODY =
       assume c: C
          we proceed by induction on c to prove csubv c c
             case CSort : n:nat ⇒
                the thesis becomes csubv (CSort n) (CSort n)
                   by (csubv_sort .)
csubv (CSort n) (CSort n)
             case CHead ⇒
                we need to prove ∀c0:C.(csubv c0 c0)→∀k:K.∀t:T.(csubv (CHead c0 k t) (CHead c0 k t))
                    assume c0: C
                    suppose H: csubv c0 c0
                    assume k: K
                      we proceed by induction on k to prove ∀t:T.(csubv (CHead c0 k t) (CHead c0 k t))
                         case Bind : b:B ⇒
                            the thesis becomes ∀t:T.(csubv (CHead c0 (Bind b) t) (CHead c0 (Bind b) t))
                               assume t: T
                                  by (csubv_bind_same . . H . . .)
                                  we proved csubv (CHead c0 (Bind b) t) (CHead c0 (Bind b) t)
∀t:T.(csubv (CHead c0 (Bind b) t) (CHead c0 (Bind b) t))
                         case Flat : f:F ⇒
                            the thesis becomes ∀t:T.(csubv (CHead c0 (Flat f) t) (CHead c0 (Flat f) t))
                               assume t: T
                                  by (csubv_flat . . H . . . .)
                                  we proved csubv (CHead c0 (Flat f) t) (CHead c0 (Flat f) t)
∀t:T.(csubv (CHead c0 (Flat f) t) (CHead c0 (Flat f) t))
                      we proved ∀t:T.(csubv (CHead c0 k t) (CHead c0 k t))
∀c0:C.(csubv c0 c0)→∀k:K.∀t:T.(csubv (CHead c0 k t) (CHead c0 k t))
          we proved csubv c c
       we proved ∀c:C.(csubv c c)