proposition: Lemma mkEns_Finite : forall s, Finite _ (!!s).
proof: Proof. intro s; pattern s; apply set_induction; clear s; intros. - intros; replace (!!s) with (Empty_set elt); auto with sets. symmetry; apply Extensionality_Ensembles. apply Empty_Empty_set; auto. - replace (!!s') with (Add _ (!!s) x). + constructor 2; auto. + symmetry; apply Extensionality_Ensembles. apply Add_Add; auto. Qed.
imports: Ensembles Finite_sets MSetInterface MSetProperties OrdersEx