DEFINITION abst_dec()
TYPE =
       ∀u:T
         .∀v:T
           .or
             ex T λt:T.eq T u (THead (Bind Abst) v t)
             ∀t:T.(eq T u (THead (Bind Abst) v t))→∀P:Prop.P
BODY =
Show proof