proposition: Lemma eq_nth_iff A n (v1 v2: t A n): (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
proof: Proof. split. - revert n v1 v2; refine (@rect2 _ _ _ _ _). + reflexivity. + intros n ? ? H ? ? H0. f_equal. * apply (H0 Fin.F1 Fin.F1 eq_refl). * apply H. intros p1 p2 H1; apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)). - intros; now f_equal. Qed.
imports: VectorDef PeanoNat Eqdep_dec