DEFINITION terms_props__kind_dec()
TYPE =
       ∀k1:K.∀k2:K.(or (eq K k1 k2) (eq K k1 k2)→∀P:Prop.P)
BODY =
Show proof