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 =
Show proof