proposition: Lemma Vnth_in : forall n (v : vector A n) k (h : k<n), Vin (Vnth v h) v.
proof: Proof. induction v. intros. absurd (k<0); lia. intro. destruct k; simpl. auto. intro. right. apply IHv. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)