There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar statements that HOL is weaker than CoC or similar because of the lack of dependent types.

Can someone explain what this means? For example, can someone give an example for X and explain why this is not possible to formalize in a system like HOL?