proposition: Lemma Vnth_opt_filter_Some_intro : forall p (xs : vector A p) n (ks : vector nat n) i (hi : i<n) (h : Vnth ks hi < p), Vnth (Vopt_filter ks xs) hi = Some (Vnth xs h).
proof: Proof. intros p xs. induction ks; intros i hi. exfalso. lia. rename h into k. simpl. destruct i as [|i]; intro hj. 2: fo. destruct (lt_dec k p). 2: lia. f_equal. apply Vnth_eq. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)