DEFINITION binder_dec()
TYPE =
       ∀t:T
         .or
           ex_3 B T T λb:B.λw:T.λu:T.eq T t (THead (Bind b) w u)
           ∀b:B.∀w:T.∀u:T.(eq T t (THead (Bind b) w u))→∀P:Prop.P
BODY =
Show proof