proposition: Lemma partition_by_prop_true : forall a, partition_by_prop a = true -> P a.
proof: Proof. intros. unfold partition_by_prop in H. destruct (P_dec a). hyp. discr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)