proposition: Lemma Vnth_eq : forall n (v : vector A n) i1 (h1 : i1<n) i2 (h2 : i2<n), i1 = i2 -> Vnth v h1 = Vnth v h2.
proof: Proof. induction v; intro; case i1. intro. absurd (0 <= 0); lia. intros n h1. absurd (0 <= S n); lia. intros. subst i2. refl. intros. subst i2. simpl. apply IHv. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)