I have a historical question: When did indexed finite types

```
Inductive fin : nat -> Type :=
| Zero: forall n, fin (S n)
| Succ: forall n, fin n -> fin (S n).
```

appear first in Coq or elsewhere?

I checked Martin-Löf, but there finite types are obtained with n constructors, not just 2. The above definition appears in Chlipala’s CPDT. I did not find it in Coq’Art.

Related: When did the recursive version with option types appear first?

```
Fixpoint Fin (n: nat) : Type :=
match n with
| 0 => False
| S n' => option (Fin n')
end.
```

Thanks in advance. Gert