 Much like in the propositional case, one may exploit this fact to give a more sophisticated translation from pure quantificational logic into intuitionistic quantificational logic. Details are given in Moschovakis (2010).