proposition: Lemma Vnth_vec_of_list : forall l d i (Hi : i < length l), Vnth (vec_of_list l) Hi = nth i l d.
proof: Proof. induction l. simpl. intros. lia. intros. rewrite vec_of_list_cons. destruct i; simpl; auto. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)