Constructively, a proof that a set is inhabited is exactly an element of that set, so if we know the set is inhabited we can just pick that element. OTOH, if w

Constructively, a proof that a set is inhabited is exactly an element of that set, so if we know the set is inhabited we can just pick that element. OTOH, if we only know the set is non-empty we cannot pick an element from it. Because assume we could. Let P be a truth value and let S={x in {1} | P}. From not not P, prove S is non-empty, so by assumption we can pick an element of it, so it is inhabited. If it is inhabited, then P. We've just proved P from not not P.