path_vector@{i} (A : Type@{i}) {n : nat} (v1 v2 : Vector@{i} A n) (H : forall i (H : (i < n)%nat), entry v1 i = entry v2 i) : v1 = v2. Proof. rapply path_sigma_hprop@{i i i}. snrapply path_list_nth'. 1: exact (pr2 v1 @ (pr2 v2)^). intros i Hi. snrefine (_ @ H i (pr2 v1 # Hi) @ _). 1, 2: apply nth'_nth'. Defined.
Require Import Basics.Overture Basics.Trunc Basics.Tactics Basics.PathGroupoids. Require Import Types.Sigma. Require Import Algebra.AbGroups.AbelianGroup Algebra.Rings.Ring Algebra.Rings.Module. Require Import Spaces.Nat.Core. Require Import Spaces.List.Core Spaces.List.Theory Spaces.List.Paths. Require Import abstract_algebra.