proposition: Lemma bool_of_rel_true x y : bool_of_rel x y = true <-> R x y.
proof: Proof. unfold bool_of_rel. split; destruct (R_dec x y). auto. discr. refl. tauto. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)