proposition: Lemma cardinal_set_eq (A B : set) : A == B -> # A = # B.
proof: Proof. intros E. unfold "#". f_equal. induction enum_X as [| a l IHl]; simpl. reflexivity. rewrite E. destruct (B a); simpl; congruence. Qed.
imports: Lists.List ZArith Setoid Coq.Classes.Morphisms Lia