proposition: Lemma cardinal_elim : forall (X:Ensemble U) (p:nat), cardinal U X p -> match p with | O => X = Empty_set U | S n => Inhabited U X end.
proof: Proof. intros X p C; elim C; simpl; trivial with sets. Qed.
imports: Ensembles Constructive_sets