proposition: Lemma Vnth_opt_filter : forall p (xs : vector A p) n (ks : vector nat n) i (hi : i<n), Vnth (Vopt_filter ks xs) hi = match lt_dec (Vnth ks hi) p with | left h => Some (Vnth xs h) | _ => None end.
proof: Proof. intros p xs. induction ks; intros i hi. lia. simpl. destruct i as [|i]. destruct (lt_dec h p); refl. apply IHks. Qed.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)