§ Parameter verus Index

• Parameters are fixed for all constructors, indexes can vary amongst constructors.
• Parameters represent parametric polymorphism, and one does not gain information on them during pattern matching.
• Indexes rep
• Coq calls indexes "non-uniform".