fact: Definition dec_rel {X:Type} (R : X → X → Prop) := ∀ x y, {R x y} + {not (R x y)}.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality)