@h4ckernews pretty much all of that applies to Agda and Rocq as well, although Lean's metaprogramming is more powerful. Then again Agda's dependently typed programming features are much more ergonomic than the others