Yes, I came here to say precisely that. It looks like it has about the same things available as coq as far as syntax is concerned, so what are the differences?
For example, they emphasise that function extensionality is a theorem here: https://arend-lang.github.io/about/arend-features (not true in CIC).
It would just be nice to see a list of the rules.
Still I don't want to get hung up on this; the rules must exist somewhere and presumably will become more discoverable. The project looks superb.