DEFINITION ty3_repellent()
TYPE =
       ∀g:G
         .∀c:C
           .∀w:T
             .∀t:T
               .∀u1:T
                 .ty3 g c (THead (Bind Abst) w t) u1
                   →∀u2:T
                        .ty3 g (CHead c (Bind Abst) w) t (lift (S O) O u2)
                          →(pc3 c u1 u2)→∀P:Prop.P
BODY =
Show proof