DEFINITION ty3_gen_cvoid()
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 Void) u)
                            →∀a:C
                                 .drop (S O) d c a
                                   →ex3_2 T T λy1:T.λ:T.eq T t1 (lift (S O) d y1) λ:T.λy2:T.eq T t2 (lift (S O) d y2) λy1:T.λy2:T.ty3 g a y1 y2
BODY =
Show proof