proposition: Lemma the_least_unicity {M: Type} {Lt} {inh : InH M} {WO: WO Lt} (X: Ensemble M) (HX: Inhabited X) : exists! l , least_member Lt X l.
proof: Proof. destruct HX as [x Hx]. case WO; intros. destruct (well_order0 X x Hx) as [x0 H0]. exists x0; split; auto. intros; eapply least_member_unicity;eauto . Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)