Ok, so the proof ordering is considered part of the program, I assumed it was an external input to be universally quantified. Thanks for the clarification.
Ok, so the proof ordering is considered part of the program, I assumed it was an external input to be universally quantified. Thanks for the clarification.