DEFINITION arity_repellent()
TYPE =
       ∀g:G
         .∀c:C
           .∀w:T
             .∀t:T
               .∀a1:A
                 .arity g (CHead c (Bind Abst) w) t a1
                   →∀a2:A.(arity g c (THead (Bind Abst) w t) a2)→(leq g a1 a2)→∀P:Prop.P
BODY =
Show proof