I am afraid that the only way to simplify is to not use the type “vector”, i.e. a list should not have its length in its type. Just use traditional lists, when you prove something about a length, use the “length” function.

Proper Treatment 正當作法/
blog/
posts/
Dependent equality/
discussion 討論

I am afraid that the only way to simplify is to not use the type “vector”, i.e. a list should not have its length in its type. Just use traditional lists, when you prove something about a length, use the “length” function.