proposition: Lemma rel_dec_bool : rel_dec -> {f : A->A->bool | fun_rel_dec f}.
proof: Proof. intro H. exists (fun x y : A => if H x y then true else false). intros x y. destruct (H x y); trivial. Qed.
imports: Coq(Relations) CoLoR(LogicUtil)