proposition: Lemma Vnth_vec_opt_of_list A : forall i m (l : list A) (im : i < m) (il : i < length l), Vnth (vec_opt_of_list m l) im = Some (ith il).
proof: Proof. induction i. destruct m. lia. destruct l. simpl; lia. refl. destruct m. lia. destruct l. simpl; lia. simpl. intros im il. erewrite IHi. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)