§ 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.