DEFINITION ty3_gen_cabbr()
TYPE =
       ∀g:G
         .∀c:C
           .∀t1:T
             .∀t2:T
               .ty3 g c t1 t2
                 →∀e:C
                      .∀u:T
                        .∀d:nat
                          .getl d c (CHead e (Bind Abbr) u)
                            →∀a0:C
                                 .csubst1 d u c a0
                                   →∀a:C
                                        .drop (S O) d a0 a
                                          →ex3_2 T T λy1:T.λ:T.subst1 d u t1 (lift (S O) d y1) λ:T.λy2:T.subst1 d u t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
BODY =
Show proof