This paper discusses advantages and disadvantages of some possible alternatives for inference rules that handle quantifiers in the proof format of the SMT-solver veriT. The quantifier-handling modules in veriT being fairly standard, we hope this will motivate the discussion among the PxTP audience around proof production for quantifier handling. This could generate ideas to help us improve our proof production module, and also benefit the SMT community.