proposition: Lemma Vnth_opt_filter_Some_elim : forall p (xs : vector A p) n (ks : vector nat n) i (hi : i<n) x, Vnth (Vopt_filter ks xs) hi = Some x -> exists h : Vnth ks hi < p, x = Vnth xs h.
proof: Proof. intros p xs. induction ks; intros i hi x. lia. rename h into k. simpl. destruct i as [|i]. 2: fo. destruct (lt_dec k p). 2: discr. intro hx; inversion hx. exists l. refl. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)