proposition: Lemma isempty_dec : forall P, finite P -> {isempty P}+{notempty P}.
proof: Proof. unfold isempty,notempty; destruct 1; auto. right; red; intros. apply (@equiv_add_empty x Q); auto. apply equiv_trans with P; auto. Qed.
imports: Coq(Arith) Coq(Lt)