DEFINITION csubc_csuba()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(csubc g c1 c2)→(csuba g c1 c2)
BODY =
        assume g: G
        assume c1: C
        assume c2: C
        suppose H: csubc g c1 c2
          we proceed by induction on H to prove csuba g c1 c2
             case csubc_sort : n:nat ⇒
                the thesis becomes csuba g (CSort n) (CSort n)
                   by (csuba_refl . .)
csuba g (CSort n) (CSort n)
             case csubc_head : c3:C c4:C :csubc g c3 c4 k:K v:T ⇒
                the thesis becomes csuba g (CHead c3 k v) (CHead c4 k v)
                (H1) by induction hypothesis we know csuba g c3 c4
                   by (csuba_head . . . H1 . .)
csuba g (CHead c3 k v) (CHead c4 k v)
             case csubc_void : c3:C c4:C :csubc g c3 c4 b:B H2:not (eq B b Void) u1:T u2:T ⇒
                the thesis becomes csuba g (CHead c3 (Bind Void) u1) (CHead c4 (Bind b) u2)
                (H1) by induction hypothesis we know csuba g c3 c4
                   by (csuba_void . . . H1 . H2 . .)
csuba g (CHead c3 (Bind Void) u1) (CHead c4 (Bind b) u2)
             case csubc_abst : c3:C c4:C :csubc g c3 c4 v:T a:A H2:sc3 g (asucc g a) c3 v w:T H3:sc3 g a c4 w ⇒
                the thesis becomes csuba g (CHead c3 (Bind Abst) v) (CHead c4 (Bind Abbr) w)
                (H1) by induction hypothesis we know csuba g c3 c4
                   (h1) 
                      by (sc3_arity_gen . . . . H2)
arity g c3 v (asucc g a)
                   end of h1
                   (h2) 
                      by (sc3_arity_gen . . . . H3)
arity g c4 w a
                   end of h2
                   by (csuba_abst . . . H1 . . h1 . h2)
csuba g (CHead c3 (Bind Abst) v) (CHead c4 (Bind Abbr) w)
          we proved csuba g c1 c2
       we proved ∀g:G.∀c1:C.∀c2:C.(csubc g c1 c2)→(csuba g c1 c2)