proposition: Theorem least_member_ex_unique : forall X x (inhX: In X x), exists! a, least_member X a.
proof: Proof. intros;destruct (well_order X x); auto. exists x0; split; auto. intros; eapply least_member_unicity;eauto. Qed.
imports: Coq(Relations Classical Classical_sets RelationClasses Wf_nat) hydras(PartialFun)