proposition: Lemma card_empty_gen (h : finite empty) : card h = 0.
proof: Proof. cut (card h <= 0). lia. change (card h <= length (@nil A)). assert (e : Pf_equiv h (finite_of_list nil)). fo. rewrite e. apply card_of_list_le_length. Qed.
imports: Coq(Basics Morphisms Setoid) CoLoR(ClassicUtil IotaUtil EpsilonUtil LogicUtil NatUtil FunUtil ListUtil ListNodup SetUtil BoundNat)