**Describe the error** The [section for recursors](https://lean-lang.org/doc/reference/latest///////The-Type-System/Inductive-Types/#recursor-types) lists four things that appear in a recursor: - parameters - the motive - _minor premises_ - the major premise, or target. The examples below talk about parameters, motive, _cases_ and target, and never about minor premises: > There are cases for both constructors, in which the motive is satisfied for both [false](https://lean-lang.org/doc/reference/latest///////Basic-Types/Booleans/#Bool___false) and [true](https://lean-lang.org/doc/reference/latest///////Basic-Types/Booleans/#Bool___false). > There are cases for both constructors: > The case for nil applies the motive to nil's index value true. > The case for cons abstracts over the index value used in its recursive occurrence, and instantiates the motive with its negation. **Why is it incorrect and/or confusing?** Consistent use of terminology is good, and being able to easily match bits of examples to bits of text helps me understand the material better.