Although I have no idea what documentation in Coq should look like to account for dependent types.
I'm pretty sure all it takes is just starting something, but as always people are busy.
@lyxia well to be honest i don’t know where to start. ):
Welcome to your niu world ! We are a cute and loving international community Ｏ(≧▽≦)Ｏ !