Here we shall consider various more substantial examples of such "higher-order" propositions. First, observe that the when quantification over propositions and properties (proposition valued functions) is permitted, then the other standard connectives and equality can all be characterized purely in terms of universal quantification and implication:
Thm* A & B (C:Prop. (A B C) C) Thm* A B (C:Prop. (A C) (B C) C) Thm* False (C:Prop. C) Thm* B:(AProp). (x:A. B(x)) (C:Prop. (x:A. B(x) C) C) Thm* a,b:A. a = b (P:(AProp). P(a) P(b)) Thm* A (C:Prop. A C) Thm* True (C:Prop. C C) Thm* (A B) (C:Prop. ((A B) (B A) C) C)
The simplicity of these characterizations leads one to consider simply adopting them as definitions in the first place, and indeed it is not unusual to do so in standard developments of higher-order logic. But we cannot do so because we have constrained ourselves to a so-called "predicative" logic (a term of Bertrand Russell's of uncertain etymology), which requires layering propositions into a hierarchy in a way that precludes us from giving the desired definitions. See
Here's another example asserting the definability of properties by structural recursion on lists, given base case
Thm* R:(A(A List)PropProp).
Thm* P:((A List)Prop).
Thm* (P(nil) Q) & (a:A, x:A List. P(a.x) R(a,x,P(x)))
Equality on the type
One case of particular note is that