DEFINITION csubt_csuba()
TYPE =
       ∀g:G.∀c1:C.∀c2:C.(csubt g c1 c2)→(csuba g c1 c2)
BODY =
        assume g: G
        assume c1: C
        assume c2: C
        suppose H: csubt g c1 c2
          we proceed by induction on H to prove csuba g c1 c2
             case csubt_sort : n:nat ⇒
                the thesis becomes csuba g (CSort n) (CSort n)
                   by (csuba_refl . .)
csuba g (CSort n) (CSort n)
             case csubt_head : c3:C c4:C :csubt g c3 c4 k:K u:T ⇒
                the thesis becomes csuba g (CHead c3 k u) (CHead c4 k u)
                (H1) by induction hypothesis we know csuba g c3 c4
                   by (csuba_head . . . H1 . .)
csuba g (CHead c3 k u) (CHead c4 k u)
             case csubt_void : c3:C c4:C :csubt 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 csubt_abst : c3:C c4:C :csubt g c3 c4 u:T t:T H2:ty3 g c3 u t :ty3 g c4 u t ⇒
                the thesis becomes csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
                (H1) by induction hypothesis we know csuba g c3 c4
                   (H_x) 
                      by (ty3_arity . . . . H2)
ex2 A λa1:A.arity g c3 u a1 λa1:A.arity g c3 t (asucc g a1)
                   end of H_x
                   (H4) consider H_x
                   we proceed by induction on H4 to prove csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
                      case ex_intro2 : x:A H5:arity g c3 u x H6:arity g c3 t (asucc g x) ⇒
                         the thesis becomes csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
                            by (csuba_arity . . . . H5 . H1)
                            we proved arity g c4 u x
                            by (csuba_abst . . . H1 . . H6 . previous)
csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
csuba g (CHead c3 (Bind Abst) t) (CHead c4 (Bind Abbr) u)
          we proved csuba g c1 c2
       we proved ∀g:G.∀c1:C.∀c2:C.(csubt g c1 c2)→(csuba g c1 c2)