On the proof theory of type two functionals based on primitive recursive operations