Inductive array (T:Type) : nat -> Type :=
| ar_empty : array T 0
| ar_ext : forall n, T -> array T n -> array T (S n).