Unify terminology around indexed families

[david-christiansen]

What question should the reference manual answer?

From Zulip:

The concept referred to as an "inductive family" in TPiL seems to be called an "indexed family" in the language reference. I believe these refer to the same thing. Could you consider unifying the terminology? (This inconsistency in terminology has caused some confusion within the Japanese Lean community.)

TPiL: https://lean-lang.org/theorem_proving_in_lean4/inductive_types.html#inductive-families
Reference: https://lean-lang.org/doc/reference/latest//The-Type-System/Inductive-Types/#inductive-datatypes-parameters-and-indices

This is a useful thing to do.