proposition: Lemma card_singleton a : card (Pf_singleton a) = 1.
proof: Proof. rewrite Pf_singleton_eq, card_add, card_empty. destruct (dec (mem a Pf_empty)). firstorder with arith. refl. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)