Example of a function that you can write in Calculus of Constructions but not in System-F It's been suggested in an answer to this question that the Calculus of Constructions has more computational strength than System-F. What are examples of functions that you express in CoC that you cannot write in System-F?
Since the CoC has dependent types and system $F$ does not, I'll assume you mean a function whose types is in system $F$, but whose definition can only be written in CoC. Luckily in this case we can restrict to system $F_\omega$, which can express the same non-dependent functions as CoC, by some erasure argument.

In general, a rule of thumb to construct such functions is to consider systems $F$ and $F_\omega$ as the language of realizers of theorems of 2-nd and higher-order arithmetic, respectively, and to prove a theorem of the form $\forall x, \exists y, P$ in one not provable in the other, which by extraction should be a function definable in one and not the other.

One such theorem is the proof of normalization of system $F$ itself, which is provable in higher-order arithmetic using the "standard" proof, and not in 2nd order arithmetic by a simple diagonalization argument (though it is instructive to see where the standard proof fails).

Extracting this gives a normalization function for encodings of system $F$ terms, definable in system $F_\omega$, but not in system $F$.

I've explained this a bit in a related answer.