DEFINITION terms_props__flat_dec()
TYPE =
       ∀f1:F.∀f2:F.(or (eq F f1 f2) (eq F f1 f2)→∀P:Prop.P)
BODY =
Show proof