proposition: Lemma Forall_nth A: forall P n (v : t A n), Forall P v <-> forall p, P (nth v p).
proof: Proof. intros P n v. split. - intros H. induction H. + apply Fin.case0. + intros p. now apply (Fin.caseS' p). - induction v as [|a v n IH]. + intros ?. constructor. + intros H. constructor. * apply (H Fin.F1). * apply IH. intros p. apply (H (Fin.FS p)). Qed.
imports: VectorDef PeanoNat Eqdep_dec