DEFINITION csubt_ty3_ld()
TYPE =
       ∀g:G
         .∀c:C
           .∀u:T
             .∀v:T
               .ty3 g c u v
                 →∀t1:T
                      .∀t2:T
                        .(ty3 g (CHead c (Bind Abst) v) t1 t2)→(ty3 g (CHead c (Bind Abbr) u) t1 t2)
BODY =
        assume g: G
        assume c: C
        assume u: T
        assume v: T
        suppose H: ty3 g c u v
        assume t1: T
        assume t2: T
        suppose H0: ty3 g (CHead c (Bind Abst) v) t1 t2
          by (csubt_refl . .)
          we proved csubt g c c
          by (csubt_abst . . . previous . . H H)
          we proved csubt g (CHead c (Bind Abst) v) (CHead c (Bind Abbr) u)
          by (csubt_ty3 . . . . H0 . previous)
          we proved ty3 g (CHead c (Bind Abbr) u) t1 t2
       we proved 
          ∀g:G
            .∀c:C
              .∀u:T
                .∀v:T
                  .ty3 g c u v
                    →∀t1:T
                         .∀t2:T
                           .(ty3 g (CHead c (Bind Abst) v) t1 t2)→(ty3 g (CHead c (Bind Abbr) u) t1 t2)