- Lists indexed by their length.
- The Vec type.
- Primitive functions.
- The proposition that a list contains some element.
- The proposition that all elements of one list are contained in another.
- Propositional and boolean John-Major equality for Vec.
- John Major propositional equality for Vec.
- Boolean equality for Vec.
- Reversing functions and induction principles
- Facts about rev
- Reverse induction principle on Vec
- Left-recursive induction principle on Vec
This page has been generated by coqdoc