DEFINITION term_dec()
TYPE =
       ∀t1:T.∀t2:T.(or (eq T t1 t2) (eq T t1 t2)→∀P:Prop.P)
BODY =
Show proof