proposition: Lemma sup_unicity : forall X l l', (Countable X /\ forall x, X x -> ordinal x) -> sup_spec X l -> sup_spec X l' -> l = l'.
proof: Proof. intros X l l' _ H H0; apply le_antisym. destruct H, H0; intuition. case (H4 l' H0);auto with schutte. destruct H, H0; intuition. case (H5 l H);auto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)