proposition: Lemma Forall_nth_order A: forall P n (v : t A n), Forall P v <-> forall i (Hi : i < n), P (nth_order v Hi).
proof: Proof. intros P n v. rewrite Forall_nth. split. - intros H i Hi. apply H. - intros H p. rewrite <- (Fin.of_nat_to_nat_inv p). apply H. Qed.
imports: VectorDef PeanoNat Eqdep_dec