3 ms·

I agree. One could argue that Agda and Idris are a better interface to the type theory that underlies Coq.