§ Parameters cannot be changed anywhere , not just in return location
inductive List (a: Type): Type where
| Good: List a
| Good2: List a -> List a
| Bad: List b -> List a
^^^^^^^ -- not allowed!
- In hindsight, this makes sense, as the parameter really is a trick to represent, well, parametric polymorphism.