proposition: Lemma bool_of_rel_refl x : Reflexive R -> bool_of_rel x x = true.
proof: Proof. intro R_refl. unfold bool_of_rel. destruct (R_dec x x). refl. exfalso. apply n. refl. Qed.
imports: Coq(Setoid Basics Morphisms List Lia) CoLoR(LogicUtil)