proposition: Lemma Included_Strict_Included : forall X Y:Ensemble U, Included U X Y -> Strict_Included U X Y \/ X = Y.
proof: Proof. intros X Y H'; try assumption. elim (classic (X = Y)); auto with sets. Qed.
imports: Ensembles Constructive_sets Classical