proposition: Lemma In_nth A: forall n (v : t A n) p, In (nth v p) v.
proof: Proof. intros n v. induction v as [|a n v IH]. - apply Fin.case0. - intros p. apply (Fin.caseS' p). + apply In_cons_hd. + intros q. apply In_cons_tl, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec