proposition: Lemma partition_by_rel_true : forall a b, partition_by_rel (a, b) = true -> R a b.
proof: Proof. intros. unfold partition_by_rel in H. simpl in H. destruct (R_dec a b). hyp. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)