proposition: Lemma card_empty : card Pf_empty = 0.
proof: Proof. apply card_empty_gen. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)