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