Some argue that Lean breaks a few type-theoretical properties. See full discussion here:

https://github.com/rocq-prover/rocq/issues/10871