proposition: Lemma Vfilter_eq_notin : forall A n (l : list (N n)) i (vi : vector A i) t u j (vj : vector A j) (e : i+S j=n), (forall hi : i<n, ~In (N_ hi) l) -> Vfilter l (Vcast (Vapp vi (Vcons t vj)) e) = Vfilter l (Vcast (Vapp vi (Vcons u vj)) e).
proof: Proof. induction l; simpl; intros. refl. apply Vcons_eq. split. rewrite !Vnth_cast, !Vnth_app. destruct a as [k h]. unfold N_val; simpl proj1_sig. case (le_gt_dec i k); intro. rewrite !Vnth_cons. case (lt_ge_dec 0 (k-i)); intro. refl. assert (k=i). lia. subst k. ded (H h). fo. refl. apply IHl. fo. Qed.
imports: CoLoR(VecUtil ListUtil NatUtil LogicUtil ListNodup BoundNat)