This PR reviews the implicitness of arguments across List/Array/Vector,
generally trying to make arguments implicit where possible, although
sometimes correcting propositional arguments which were incorrectly
implicit to explicit.
This PR adds basic lemmas about lexicographic order on Array and Vector,
achieving parity with List.
Many lemmas are still missing for all three, particularly about how
order interacts with `++`.
