Axiom audit for the direct parallel repetition theorems

The theorems proved through the vendored developments must not depend on anything beyond the three standard axioms; this file fails to build otherwise.