proposition: Lemma characteristic_function_to_ensemble_is_identity: forall {X:Type} (P:X->Prop), [ x:X | P x ] = P.
proof: Proof. intros. apply Extensionality_Ensembles; split; red; intros. destruct H. exact H. constructor. exact H. Qed.
imports: Ensembles EnsemblesImplicit