proposition: Lemma list_of_vec_exact : forall i n (v : vector A n) (Hi : i < n), element_at (list_of_vec v) i = Some (Vnth v Hi).
proof: Proof. induction i; intros. destruct v; simpl in *. contradict Hi; lia. auto. destruct v; simpl in *. contradict Hi; lia. apply IHi. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)