  Here we recall the disjunction and existence properties, formulated for a set theory \(T\). The informal motivation for the disjunction and  the existence properties is based on our understanding of the constructive proofs of disjunctive and existential statements (respectively).  In fact, it seems reasonable to expect that if we constructively prove  a disjunction \(\phi \vee \psi\),  then we should also be able to prove \(\phi\) or prove \(\psi\).  Similarly, if we prove an existential statement, then we should be  able to prove that a witness to that statement is definable within our theory.