In $\lambda P2$, we can write polymorphic functions like $\Lambda A. \lambda x. x: \Pi A. A \to A$. By Curry–Howard, this corresponds to the proposition "for all propositions $A$, $A$ implies $A$". From my understanding, the quantification here is predicative, i.e. "for all propositions" includes the proposition "for all propositions $A$, $A$ implies $A$" itself. Hence, $\lambda P2$ allows quantifying over arbitrary propositions.
If so, then I'm wondering about the difference between $\lambda P2$ and COC. From my understanding, the logical difference between $\lambda P2$ and COC is that COC allows predicates over propositions. Supposedly, $\lambda P2$ logically corresponds to second-order predicate calculus, while COC is higher-order predicate calculus.
But why is $\lambda P2$ only second-order? Isn't a statement like "for all propositions $A$, $A$ implies $A$" already a higher-order statement, because it not only quantifies first-order statements, but also second-order statements, etc.? If not, how does adding predicates over propositions make COC higher-order? What's an example of a higher-order proposition we can make in COC that we can't in $\lambda P2$?