diff --git a/theories/Compat/Fin92.v b/theories/Compat/Fin92.v
new file mode 100644
index 0000000000..f4a0f23093
--- /dev/null
+++ b/theories/Compat/Fin92.v
@@ -0,0 +1,119 @@
+From Stdlib Require Import PeanoNat Peano_dec.
+Local Open Scope nat_scope.
+
+Inductive fin : nat -> Type :=
+| finO {n}             : fin (S n)
+| finS {n} (_ : fin n) : fin (S n).
+Notation t := fin (only parsing).
+Notation fin0 := finO (only parsing).
+
+Fixpoint to_nat {n} (i : fin n) : nat :=
+  match i with
+  | finO => 0
+  | finS i => S (to_nat i)
+  end.
+Coercion to_nat : fin >-> nat.
+
+Definition cast {m} (v: t m) {n} : m = n -> t n :=
+  match Nat.eq_dec m n with
+  | left Heq => fun _ => eq_rect m _ v n Heq
+  | right Hneq => fun Heq => False_rect _ (Hneq Heq)
+  end.
+
+Fixpoint add_nat (n : nat) [m] (i : fin m) {struct n} : fin (n + m) :=
+  match n with
+  | 0 => i
+  | S n => finS (add_nat n i)
+  end.
+
+Section Relax.
+Context (n : nat).
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
+Fixpoint relax {m} (i : fin m) : fin (m + n) :=
+  match i in fin m return fin (m + n) with
+  | finO => finO
+  | finS i => finS (relax i)
+  end.
+End Relax.
+
+Require Import Lia.
+Definition of_nat n (i : nat) (_ : i < n) : fin n.
+  refine (cast (add_nat i (@fin0 (n-S i))) _).
+Proof. abstract lia. Defined.
+
+Lemma inj_0 (i : fin 0) : False.
+Proof. exact (match i with end). Qed.
+
+Lemma inj_S {n} (i : t (S n)) : i = finO \/ exists j, i = finS j.
+Proof.
+  pattern i; refine ( (* destruct i, but using elaborator's small inversions *)
+  match i in fin (S n) return forall P, P finO -> (forall i, P (finS i)) -> P i with
+  | finO | _ => _ end _ _ _); eauto.
+Qed.
+
+Lemma to_nat_inj [n] (i j : fin n) : to_nat i = to_nat j -> i = j.
+Proof.
+  induction i; pose proof inj_S j; firstorder subst; try discriminate;
+    cbn [to_nat] in *; eauto using f_equal.
+Qed.
+
+Lemma to_nat_inj_iff [n] (i j : fin n) : to_nat i = to_nat j <-> i = j.
+Proof. split; try apply to_nat_inj; congruence. Qed.
+
+Lemma to_nat_inj_dep [n] (i : fin n) [m] (j : fin m) : n = m -> to_nat i = to_nat j ->
+  existT _ _ i = existT _ _ j.
+Proof. destruct 1; auto using f_equal, to_nat_inj. Qed.
+
+Lemma to_nat_0 n : to_nat (@finO n) = 0.
+Proof. trivial. Qed.
+
+Lemma to_nat_S [n] (i : fin n) : to_nat (finS i) = S (to_nat i).
+Proof. trivial. Qed.
+
+Lemma to_nat_bound [n] (i : fin n) : to_nat i < n.
+Proof.
+  induction i; cbn [to_nat]. { apply Nat.lt_0_succ. }
+  rewrite <-Nat.succ_lt_mono. apply IHi.
+Qed.
+
+
+Lemma to_nat_eq_rect [m n] (p : m = n) i : to_nat (eq_rect m fin i n p) = to_nat i.
+Proof. case p; trivial. Qed.
+
+Lemma to_nat_cast [m n] (p : m = n) (i : fin m) : to_nat (cast i p) = to_nat i.
+Proof. cbv[cast]. case Nat.eq_dec; intros; [apply to_nat_eq_rect|contradiction]. Qed.
+
+Lemma cast_ext [m n] (p q : m = n) (i : fin m) : cast i p = cast i q.
+Proof. apply to_nat_inj; rewrite 2 to_nat_cast; trivial. Qed.
+
+
+Lemma to_nat_add_nat n [m] (i : fin m) : to_nat (add_nat n i) = n+i.
+Proof. induction n; cbn [to_nat add_nat Nat.add]; auto. Qed.
+
+Lemma to_nat_of_nat i n p : to_nat (of_nat n i p) = i.
+Proof.
+  cbv [of_nat].
+  rewrite to_nat_cast, to_nat_add_nat, to_nat_0, Nat.add_0_r; trivial.
+Qed.
+
+Lemma of_nat_to_nat [n] i p : of_nat n (to_nat i) p = i.
+Proof. apply to_nat_inj, to_nat_of_nat. Qed.
+
+Lemma of_nat_ext [n i] (p q : i < n) : of_nat n i p = of_nat n i q.
+Proof. apply cast_ext. Qed.
+
+
+
+Lemma finS_inj {n} (x y : fin n) : finS x = finS y -> x = y.
+Proof. rewrite <-!to_nat_inj_iff; cbn [to_nat]; congruence. Qed.
+
+
+
+Fixpoint of_nat' (i : nat) : fin (S i) :=
+  match i with
+  | O => finO
+  | S i => finS (of_nat' i)
+  end.
+
+Lemma to_nat_of_nat' i : to_nat (of_nat' i) = i.
+Proof. induction i; cbn [to_nat of_nat']; auto. Qed.
diff --git a/theories/Compat/Vector92.v b/theories/Compat/Vector92.v
new file mode 100644
index 0000000000..bfdd39eafb
--- /dev/null
+++ b/theories/Compat/Vector92.v
@@ -0,0 +1,475 @@
+From Stdlib Require Import PeanoNat List Lia.
+#[local] Set Warnings "-stdlib-vector".
+From Stdlib.Compat Require Import Fin92.
+
+#[universes(template)]
+Inductive vec A : nat -> Type :=
+| nil : vec _ 0
+| cons (h : A) (n : nat) (tl : vec _ n) : vec _ (S n).
+Arguments nil {_}.
+Arguments cons {_} _ {_} _.
+Notation t := vec (only parsing).
+
+Section UniformElementType.
+Context {A : Type}.
+
+Fixpoint to_list {n} (v : vec A n) {struct v} : list A :=
+  match v with
+  | nil => List.nil
+  | cons a v => List.cons a (to_list v)
+  end.
+
+Fixpoint of_list (l : list A) {struct l} : vec A (length l) :=
+  match l with
+  | List.nil => nil
+  | List.cons h tail => cons h (of_list tail)
+  end.
+
+Definition cast {m} (v: t A m) {n} : m = n -> t A n :=
+  match Nat.eq_dec m n with
+  | left Heq => fun _ => eq_rect m _ v n Heq
+  | right Hneq => fun Heq => False_rect _ (Hneq Heq)
+  end.
+
+Definition tl {n} (v : vec A (S n)) : vec A n := let 'cons _ v := v in v.
+
+Definition hd {n} (v : vec A (S n)) : A := let 'cons a _ := v in a.
+
+Definition hd_error {n} (v : vec A n) : option A :=
+  match v with
+  | nil => None
+  | cons a v => Some a
+  end.
+
+Fixpoint snoc {n} (v:t A n) (a : A) {struct v} : t A (S n) :=
+  match v with
+  | nil => cons a nil
+  | cons h t => cons h (snoc t a)
+  end.
+
+Fixpoint last {n} (v : vec A (S n)) {struct v} : A :=
+  let '@cons _ a n v := v in
+  match n return vec _ n -> _ with
+  | O => fun _ => a
+  | S _ => last
+  end v.
+
+Fixpoint app {n} (v : vec A n) {p} (w : vec A p) {struct v} : vec A (n+p) :=
+  match v with
+  | nil => w
+  | cons a v => cons a (app v w)
+  end.
+
+Section WithA.
+Context (a : A).
+Fixpoint repeat n {struct n} : vec A n :=
+  match n with
+  | O => nil
+  | S n => cons a (repeat n)
+  end.
+End WithA.
+
+Fixpoint firstn {n} (v : vec A n) {struct v} : forall i, vec A (Nat.min n i) :=
+  match v with
+  | nil => fun _ => nil
+  | cons a v => fun i =>
+      match i with
+      | O => nil
+      | S i => cons a (firstn v i)
+      end
+  end.
+
+Succeed
+Fixpoint skipn (i : nat) {n} (v : vec A n) {struct i} : vec A (Nat.sub n i) :=
+  match i with
+  | O => cast v (eq_sym (Nat.sub_0_r n))
+  | S i =>
+      match v with
+      | nil => nil
+      | cons a v => skipn i v
+      end
+  end.
+
+Fixpoint skipn {n} (v : vec A n) i {struct v} : vec A (Nat.sub n i) :=
+  match v with
+  | nil => match i with (O|_) => nil end
+  | (cons a v') as v =>
+      match i with
+      | O => v
+      | S i => skipn v' i
+      end
+  end.
+
+Succeed
+Fixpoint get {n : nat} (v : vec A n) (i : nat) {struct v} :=
+  match v with
+  | nil => None
+  | cons a v =>
+    match i with
+    | O => Some a
+    | S i => get v i
+    end
+  end.
+
+Definition get {n} (v : vec A n) i := hd_error (skipn v i).
+
+Fixpoint put {n : nat} (v : vec A n) (i : nat) (a : A) {struct v} :=
+  match v with
+  | nil => nil
+  | cons b v =>
+    match i with
+    | O => cons a v
+    | S i => cons b (put v i a)
+    end
+  end.
+
+Section WithI.
+Context (i : nat).
+Definition lastn {n} (v : vec A n) : vec A (Nat.min n i).
+(*
+refine
+  match Nat.eq_dec n (Nat.min n i) with
+  | left Heq => eq_rect _ _ v _ Heq
+  | right Hneq =>
+    match v in vec _ n return _ -> vec _ (Nat.min n _) with
+    | nil => fun _ => nil
+    | @cons _ a n' v => fun _ => cast (@lastn _ v) _
+    end Hneq
+  end.
+ *)
+refine (cast (skipn v (n-i)) _).
+abstract lia.
+Defined.
+End WithI.
+
+Fixpoint unappl {i n} {struct i} : forall (v : vec A (i+n)), vec A i :=
+  match i with
+  | O => fun v => nil
+  | S i => fun v => cons (hd v) (unappl (tl v))
+  end.
+
+Fixpoint unappr {i n} {struct i} : forall (v : vec A (i+n)), vec A n :=
+  match i with
+  | O => fun v => v
+  | S i => fun v => unappr (tl v)
+  end.
+
+Fixpoint unapp (l : nat) {r : nat} : t A (l + r) -> t A l * t A r :=
+  match l with
+  | 0 => fun v => (nil, v)
+  | S l' => fun v =>
+    let (v1, v2) := unapp l' (tl v) in
+    (cons (hd v) v1, v2)
+  end.
+
+Lemma length_to_list n (v : t A n) : length (to_list v) = n.
+Proof. induction v; cbn [length to_list]; auto. Qed.
+
+Local Definition rev_append {n p} (v : vec A n) (w : vec A p) : vec A (n + p).
+  refine (cast (of_list (List.rev_append (to_list v) (to_list w))) _).
+Proof.
+  abstract (rewrite rev_append_rev, length_app, length_rev, 2 length_to_list; trivial).
+Defined.
+
+Definition rev {n} (v : vec A n) : vec A n.
+  refine (cast (of_list (List.rev (to_list v))) _).
+Proof. abstract (rewrite length_rev, length_to_list; trivial). Defined.
+End UniformElementType.
+Coercion to_list : t >-> list.
+Arguments length_to_list [A] n v.
+
+Section Map.
+Context {A} {B} (f : A -> B).
+Fixpoint map {n} (v:t A n) : t B n :=
+  match v with
+  | nil => nil
+  | cons a v' => cons (f a) (map v')
+  end.
+End Map.
+
+Section Map2.
+Context {A B C} (f : A -> B -> C).
+Fixpoint map2 {n} (v : vec A n) {struct v} : vec B n -> vec C n :=
+  match v with
+  | nil => fun _ => nil
+  | cons a v => fun w => cons (f a (hd w)) (map2 v (tl w))
+  end.
+End Map2.
+
+Section FoldLeft.
+Context {A B : Type} (f:B->A->B).
+Fixpoint fold_left (b : B) {n} (v : t A n) : B :=
+  match v with
+  | nil => b
+  | cons a v => fold_left (f b a) v
+  end.
+End FoldLeft.
+
+Section FoldRight.
+Context {A B : Type} (f : A->B->B).
+Fixpoint fold_right {n} (v : t A n) (b:B) {struct v} : B :=
+  match v with
+  | nil => b
+  | cons a v => f a (fold_right v b)
+  end.
+End FoldRight.
+
+
+Module Import VectorNotations.
+Declare Scope vector_scope.
+Delimit Scope vector_scope with vector.
+Notation "[ ]" := nil (format "[ ]") : vector_scope.
+Notation "h :: t" := (cons h t) (at level 60, right associativity)
+  : vector_scope.
+Notation "[ x ]" := (x :: nil) : vector_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons x (cons y .. (cons z nil) ..)) : vector_scope.
+Infix "++" := app : vector_scope.
+Open Scope vector_scope.
+End VectorNotations.
+
+
+Section Forall.
+Context {A} (P: A -> Prop).
+Inductive Forall : forall {n} (v : vec A n), Prop :=
+| Forall_nil : Forall nil
+| Forall_cons {n} x (v : vec A n) (_ : P x) (_ : Forall v) : Forall (cons x v).
+End Forall.
+
+Section Exists.
+Context {A} (P: A -> Prop).
+Inductive Exists : forall {n}, vec A n -> Prop :=
+| Exists_cons_hd {n} x v (_ : P x) : @Exists (S n) (cons x v)
+| Exists_cons_tl {n} x v (_ : Exists v) : @Exists (S n) (cons x v).
+End Exists.
+
+Section In.
+Context {A} (a : A).
+Inductive In : forall {n}, vec A n -> Prop :=
+| In_cons_hd {n} v : @In (S n) (cons a v)
+| In_cons_tl {n} x v (_ : In v) : @In (S n) (cons x v).
+End In.
+
+Section Forall2.
+Context {A B} (P:A->B->Prop).
+Inductive Forall2 : forall {n}, vec A n -> vec B n -> Prop :=
+| Forall2_nil : @Forall2 0 nil nil
+| Forall2_cons {n} x1 x2 v1 v2 (_ : P x1 x2) (_ : Forall2 v1 v2)
+  : @Forall2 (S n) (cons x1 v1) (cons x2 v2).
+End Forall2.
+
+Section Exists2.
+Context {A B} (P : A->B->Prop).
+Inductive Exists2 : forall {n}, vec A n -> vec B n -> Prop :=
+| Exists2_cons_hd {n} x1 x2 v1 v2 (_ :  P x1 x2) : @Exists2 (S n) (x1::v1) (x2::v2)
+| Exists2_cons_tl {n} x1 x2 v1 v2 (_ : Exists2 v1 v2) : @Exists2 (S n) (x1::v1) (x2::v2).
+End Exists2.
+
+
+Lemma inj_0 [A] (v : vec A 0) : v = nil.
+Proof. exact (let 'nil := v in eq_refl). Qed.
+ 
+Lemma inj_S [A n] (v : vec A (S n)) : v = cons (hd v) (tl v).
+Proof. exact (let 'cons _ _ := v in eq_refl). Qed.
+
+Lemma to_list_inj [A n] (v w : t A n) : to_list v = to_list w -> v = w.
+Proof.
+  induction n; cbn [to_list].
+  { rewrite (inj_0 v), (inj_0 w); trivial. }
+  { rewrite (inj_S v), (inj_S w); inversion 1; f_equal; eauto. }
+Qed.
+
+Lemma to_list_inj_iff [A n] (v w : t A n) : to_list v = to_list w <-> v = w.
+Proof. split; try apply to_list_inj; congruence. Qed.
+
+Lemma to_list_inj_dep [A m] (v : t A m) [n] (w : t A n) :
+  to_list v = to_list w -> existT _ _ v = existT _ _ w.
+Proof.
+  intros H; specialize (f_equal (@length _) H); rewrite 2 length_to_list.
+  destruct 1; auto using f_equal, to_list_inj.
+Qed.
+
+Lemma to_list_eq_rect [A m n] (p : m = n) v : to_list (eq_rect m (vec A) v n p) = to_list v.
+Proof. case p; trivial. Qed.
+
+Lemma to_list_cast [A m n] (p : m = n) (v : vec A m) : to_list (cast v p) = to_list v.
+Proof. cbv[cast]. case Nat.eq_dec; intros; [apply to_list_eq_rect|contradiction]. Qed.
+
+
+Lemma to_list_nil A : to_list (@nil A) = List.nil.
+Proof. trivial. Qed.
+
+Lemma to_list_cons [A n] a (v : t A n) : to_list (cons a v) = List.cons a v.
+Proof. trivial. Qed.
+
+Lemma to_list_of_list [A] (l : list A) : to_list (of_list l) = l.
+Proof. induction l; cbn [to_list of_list]; congruence. Qed.
+
+Lemma hd_to_list [A n] (d : A) (v : t A (S n)) : List.hd d v = hd v.
+Proof. rewrite (inj_S v); trivial. Qed.
+
+Lemma to_list_tl [A n] (v : t A (S n)) : to_list (tl v) = List.tl v.
+Proof. rewrite (inj_S v); trivial. Qed.
+
+Lemma last_to_list [A n] (d : A) (v : t A (S n)) : List.last v d = last v.
+Proof.
+  rewrite (inj_S v) in *.
+  generalize (hd v); generalize (tl v); clear v; induction v; trivial.
+  set (h::v) as hv; cbn [List.last to_list last]; subst hv. rewrite IHv. auto.
+Qed.
+
+Lemma to_list_repeat [A n] (a : A) : to_list (repeat a n) = List.repeat a n.
+Proof. induction n; cbn [to_list repeat List.repeat]; auto using f_equal2. Qed.
+
+Lemma to_list_app [A n p] (v : vec A n) (w : vec A p) : to_list (app v w) = List.app v w.
+Proof. induction v; cbn [to_list app List.app]; rewrite ?IHv; trivial. Qed.
+
+Lemma to_list_firstn [A n] (v : t A n) i : to_list (firstn v i) = List.firstn i v.
+Proof. revert i; induction v, i; cbn [to_list firstn List.firstn]; congruence. Qed.
+
+Lemma to_list_rev_append [A n p] (v : vec A n) (w : vec A p) :
+  to_list (rev_append v w) = List.app (List.rev v) w.
+Proof.
+  cbv [rev_append]. rewrite to_list_cast, rev_append_rev, !to_list_of_list; trivial.
+Qed.
+
+Lemma to_list_rev [A n] (v : vec A n) : to_list (rev v) = List.rev v.
+Proof. cbv [rev]. rewrite to_list_cast, to_list_of_list; trivial. Qed.
+
+Lemma to_list_In A a n (v : t A n): In a v <-> List.In a (to_list v).
+Proof.
+  split.
+  { induction 1; [left|right]; auto. }
+  { induction v; inversion 1; subst; auto using In_cons_tl, In_cons_hd. }
+Qed.
+
+Lemma to_list_map [A B n] (f : A -> B) (v : vec A n) : to_list (map f v) = List.map f v.
+Proof. induction v; cbn [to_list map List.map]; auto using f_equal. Qed.
+
+Lemma to_list_map2 [A B C n] (f : A -> B -> C) (v : vec A n) (w : vec B n) :
+  to_list (map2 f v w) = List.map (uncurry f) (List.combine v w).
+Proof.
+  induction v; [|rewrite (inj_S w)];
+    cbn [to_list map2 List.map List.combine]; auto using f_equal.
+Qed.
+
+Lemma to_list_snoc [A n] (v : vec A n) a : to_list (snoc v a) = List.app v (List.cons a List.nil).
+Proof. induction v; cbn; auto using f_equal. Qed.
+
+
+(** * [app] *)
+
+Lemma app_assoc_dep [A n m l] (a : vec A n) (b : vec A m) (c : vec A l) :
+  existT _ _ (app a (app b c)) = existT _ _ (app (app a b) c).
+Proof.
+  apply to_list_inj_dep.
+  induction a; cbn [app to_list]; auto using f_equal2.
+Qed.
+
+Lemma app_assoc [A n m l] (a : vec A n) (b : vec A m) (c : vec A l) :
+  app a (app b c) = cast (app (app a b) c) (eq_sym (Nat.add_assoc _ _ _)).
+Proof.
+  pose proof app_assoc_dep a b c as E; symmetry in E; inversion_sigma.
+  apply to_list_inj; rewrite <-E2, to_list_eq_rect, to_list_cast; trivial.
+Qed.
+
+Lemma sym_app_assoc [A n m l] (a : vec A n) (b : vec A m) (c : vec A l) :
+  app (app a b) c = cast (app a (app b c)) (Nat.add_assoc _ _ _).
+Proof.
+  pose proof app_assoc_dep a b c as E; inversion_sigma.
+  apply to_list_inj; rewrite <-E2, to_list_eq_rect, to_list_cast; trivial.
+Qed.
+
+Lemma app_repeat_repeat [A] (a : A) n m : app (repeat a n) (repeat a m) = repeat a (n + m).
+Proof. induction n; cbn [app repeat Nat.add]; auto using f_equal. Qed.
+
+(** * [rev] *)
+
+Lemma rev_nil A : rev nil = nil :> vec A _.
+Proof. trivial. Qed.
+
+Lemma rev_cons [A n] a (v : vec A n) : rev (cons a v) = snoc (rev v) a.
+Proof. erewrite <-to_list_inj_iff, to_list_snoc, 2 to_list_rev, to_list_cons, List.rev_cons; trivial. Qed.
+
+Lemma rev_snoc [A n] (v : vec A n) a : rev (snoc v a) = cons a (rev v).
+Proof. erewrite <-to_list_inj_iff, to_list_cons, 2 to_list_rev, to_list_snoc, List.rev_unit; trivial. Qed.
+
+Lemma rev_rev [A n] (v : vec A n) : rev (rev v) = v.
+Proof. apply to_list_inj; rewrite 2 to_list_rev, List.rev_involutive; trivial. Qed.
+
+Lemma rev_map [A B] (f : A -> B) [n] (v : t A n) : rev (map f v) = map f (rev v).
+Proof. apply to_list_inj; rewrite to_list_map, 2 to_list_rev, List.map_rev, to_list_map. trivial. Qed.
+
+Lemma map_rev [A B] (f : A -> B) [n] (v : t A n) : map f (rev v) = rev (map f v).
+Proof. apply to_list_inj; rewrite to_list_map, 2 to_list_rev, List.map_rev, to_list_map. trivial. Qed.
+
+
+(** * [map] *)
+
+Lemma map_nil [A B] (f : A -> B) : map f nil = nil.
+Proof. trivial. Qed.
+
+Lemma map_cons [A B] (f : A -> B) (a : A) [n] (v : vec A n) :
+  map f (cons a v) = cons (f a) (map f v).
+Proof. trivial. Qed.
+
+Lemma map_map [A B C] (f : A -> B) (g : B -> C) [n] (v : vec A n) :
+  map g (map f v) = map (fun x => g (f x)) v.
+Proof. apply to_list_inj; rewrite 3 to_list_map, List.map_map; trivial. Qed.
+
+Lemma map_ext_in [A B] (f g:A->B) [n] (v : t A n)
+  (H : forall a, In a v -> f a = g a) : map f v = map g v.
+Proof.  setoid_rewrite to_list_In in H; erewrite <-to_list_inj_iff, !to_list_map, List.map_ext_in; trivial. Qed.
+
+Lemma map_ext [A B] (f g:A->B) [n] (v : t A n)
+  (H : forall a, f a = g a) : map f v = map g v.
+Proof. erewrite <-to_list_inj_iff, !to_list_map, List.map_ext; trivial. Qed.
+
+Lemma map_app [A B] (f : A -> B) [n m] (v: t A n) (w: t A m) :
+  map f (v ++ w) = map f v ++ map f w.
+Proof. erewrite <-to_list_inj_iff, to_list_app, 3 to_list_map, to_list_app, List.map_app; trivial. Qed.
+
+Lemma map_snoc [A B] (f : A -> B) [n] (v : vec A n) a :
+  map f (snoc v a) = snoc (map f v) (f a).
+Proof. induction v; cbn [map snoc]; auto using f_equal. Qed.
+
+
+(** * [fold_right] *)
+
+Lemma fold_right_snoc [A B] f (a : A) (b : B) n (v : vec A n) :
+  fold_right f (snoc v a) b = fold_right f v (f a b).
+Proof. induction v; cbn [snoc fold_right]; rewrite ?IHv; trivial. Qed.
+
+Lemma fold_right_rev [A B] (f : A -> B -> B) [n] (v : vec A n) b :
+  fold_right f (rev v) b = fold_left (fun x y => f y x) b v.
+Proof.
+  revert b; induction v; intros; rewrite ?rev_nil, ?rev_cons, ?fold_right_snoc; trivial.
+Qed.
+
+
+(** * [cast] *)
+
+Lemma cast_nil [A] p : cast nil p = nil :> vec A 0.
+Proof. trivial. Qed.
+
+Lemma cast_cons [A m] a (v : vec A m) [n] p :
+  cast (cons a v) p = cons a (cast v (Nat.succ_inj _ _ p)) :> vec A (S n).
+Proof. apply to_list_inj; repeat rewrite ?to_list_cast, ?to_list_cons; trivial. Qed.
+
+Lemma cast_refl [A n] (v : vec A n) p : cast v p = v.
+Proof. apply to_list_inj; repeat rewrite ?to_list_cast; trivial. Qed.
+
+Lemma cast_ext [A m] (v : vec A m) [n] p q : cast v p = cast v q :> vec A n.
+Proof. apply to_list_inj; repeat rewrite ?to_list_cast; trivial. Qed.
+
+
+(** * [put] *)
+
+Lemma put_alt_subproof : forall x x0 : nat, Nat.min x x0 + (x - x0) = x.
+Proof. lia. Qed.
+
+Lemma put_alt [A n] (v : vec A n) (i : nat) (a : A) :
+  put v i a = cast (app (firstn v i) (match skipn v i with nil => nil | cons _ v => cons a v end)) (put_alt_subproof n i).
+Proof.
+  revert i; induction v, i; cbn [put firstn app skipn Nat.min Nat.sub Nat.add];
+    rewrite ?cast_refl, ?cast_cons, ?IHv; auto using f_equal, cast_ext.
+Qed.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index e1d3ab6ab3..6279f4c8d6 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -1007,6 +1007,9 @@ Section ListOps.
     rewrite !rev_involutive in H. assumption.
   Qed.
 
+  Lemma rev_cons (a : A) l : rev (cons a l) = rev l ++ [a].
+  Proof. apply rev_inj. rewrite rev_unit, !rev_involutive; trivial. Qed.
+
   Lemma rev_eq_app : forall l l1 l2, rev l = l1 ++ l2 -> l = rev l2 ++ rev l1.
   Proof.
     intros l l1 l2 Heq.
diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v
index a2d650ec7e..0656b30690 100644
--- a/theories/Vectors/Fin.v
+++ b/theories/Vectors/Fin.v
@@ -1,3 +1,5 @@
+Require Import Compat.Fin92.
+Local Set Warnings "-deprecated".
 (************************************************************************)
 (*         *      The Rocq Prover / The Rocq Development Team           *)
 (*  v      *         Copyright INRIA, CNRS and contributors             *)
@@ -34,14 +36,30 @@ the n-uplet. If [f] is the k-th element of the (n-1)-uplet, [FS f] is the
    Institution: PPS, INRIA 12/2010-01/2012-07/2012
 *)
 
-Inductive t : nat -> Set :=
-|F1 : forall {n}, t (S n)
-|FS : forall {n}, t n -> t (S n).
+#[deprecated(since="9.1", use=Fin92.fin)]
+Notation t := Fin92.fin (only parsing).
+#[deprecated(since="9.1", use=Fin92.finO)]
+Notation F1 := finO (only parsing).
+#[deprecated(since="9.1", use=Fin92.finS)]
+Notation FS := finS (only parsing).
+#[deprecated(since="9.1", use=Fin92.fin_ind)]
+Notation t_ind := Fin92.fin_ind (only parsing).
+#[deprecated(since="9.1", use=Fin92.fin_rect)]
+Notation t_rect := Fin92.fin_ind (only parsing).
+#[deprecated(since="9.1", use=Fin92.fin_rec)]
+Notation t_rec := Fin92.fin_ind (only parsing).
+#[deprecated(since="9.1", use=Fin92.fin_sind)]
+Notation t_sind := Fin92.fin_sind (only parsing).
+
+Arguments F1 {n}.
+Arguments FS {n} _.
 
 Section SCHEMES.
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition case0 P (p: t 0): P p :=
   match p with | F1 | FS  _ => fun devil => False_rect (@ID) devil (* subterm !!! *) end.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition caseS' {n : nat} (p : t (S n)) : forall (P : t (S n) -> Type)
   (P1 : P F1) (PS : forall (p : t n), P (FS p)), P p :=
   match p with
@@ -49,10 +67,12 @@ Definition caseS' {n : nat} (p : t (S n)) : forall (P : t (S n) -> Type)
   | FS pp => fun P P1 PS => PS pp
   end.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition caseS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t n), P (FS p))
   {n} (p: t (S n)) : P p := caseS' p P (P1 n) PS.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition rectS (P: forall {n}, t (S n) -> Type)
   (P1: forall n, @P n F1) (PS : forall {n} (p: t (S n)), P p -> P (FS p)):
   forall {n} (p: t (S n)), P p :=
@@ -63,6 +83,7 @@ fix rectS_fix {n} (p: t (S n)): P p:=
   | @FS (S k) pp => PS pp (rectS_fix pp)
   end.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition rect2 (P : forall {n} (a b : t n), Type)
   (H0 : forall n, @P (S n) F1 F1)
   (H1 : forall {n} (f : t n), P F1 (FS f))
@@ -150,6 +171,7 @@ Qed.
 (** [weak p f] answers a function witch is the identity for the p{^  th} first
 element of [fin (p + m)] and [FS (FS .. (FS (f k)))] for [FS (FS .. (FS k))]
 with p FSs *)
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Fixpoint weak {m}{n} p (f : t m -> t n) :
   t (p + m) -> t (p + n) :=
 match p as p' return t (p' + m) -> t (p' + n) with
@@ -162,9 +184,10 @@ end.
 
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (m + n)] *)
-Fixpoint L {m} n (p : t m) : t (m + n) :=
-  match p with |F1 => F1 |FS p' => FS (L n p') end.
+#[deprecated(since="9.1", use=Fin92.relax)]
+Notation L n := (relax n) (only parsing).
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma L_sanity {m} n (p : t m) : proj1_sig (to_nat (L n p)) = proj1_sig (to_nat p).
 Proof.
 induction p as [|? p IHp].
@@ -172,6 +195,7 @@ induction p as [|? p IHp].
 - simpl; destruct (to_nat (L n p)); simpl in *; rewrite IHp. now destruct (to_nat p).
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma L_inj {m} n (p q : t m) : L n p = L n q -> p = q.
 Proof.
 induction p as [m|m p IH]; apply (caseS' q); [easy..|].
@@ -181,6 +205,7 @@ Qed.
 (** The p{^ th} element of [fin m] viewed as the p{^ th} element of
 [fin (n + m)]
 Really really inefficient !!! *)
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition L_R {m} n (p : t m) : t (n + m).
 Proof.
 induction n as [|n IHn].
@@ -194,9 +219,10 @@ Defined.
 
 (** The p{^ th} element of [fin m] viewed as the (n + p){^ th} element of
 [fin (n + m)] *)
-Fixpoint R {m} n (p : t m) : t (n + m) :=
-  match n with |0 => p |S n' => FS (R n' p) end.
+#[deprecated(since="9.1", use=Fin92.add_nat)]
+Notation R n := (add_nat n) (only parsing).
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma R_sanity {m} n (p : t m) : proj1_sig (to_nat (R n p)) = n + proj1_sig (to_nat p).
 Proof.
 induction n as [|n IHn].
@@ -204,6 +230,7 @@ induction n as [|n IHn].
 - simpl; destruct (to_nat (R n p)); simpl in *; rewrite IHn. now destruct (to_nat p).
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma R_inj {m} n (p q : t m) : R n p = R n q -> p = q.
 Proof.
 induction n as [|n IH].
@@ -211,6 +238,7 @@ induction n as [|n IH].
 - intros ?. now apply IH, FS_inj.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma L_R_neq n m (p : t n) (q : t m) : L m p <> R n q.
 Proof.
 induction p as [n|n p IH].
@@ -218,6 +246,7 @@ induction p as [n|n p IH].
 - intros ?. now apply IH, FS_inj.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Fixpoint case_L_R' {n m} : forall (P : t (n + m) -> Type) (p : t (n + m)),
   (forall q, P (L m q)) -> (forall q, P (R n q)) -> P p :=
 match n with
@@ -227,10 +256,12 @@ match n with
     (fun p' => case_L_R' (fun q => P (Fin.FS q)) p' (fun q => HL (Fin.FS q)) HR)
 end.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Definition case_L_R (P : forall n m, t (n + m) -> Type) {n m} (p : t (n + m)) :
   (forall n m (q : t n), P n m (L m q)) -> (forall n m (q : t m), P n m (R n q)) -> P n m p :=
 fun HL HR => case_L_R' _ p (HL _ _) (HR _ _).
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma case_L_R'_L {n m : nat} (P : Fin.t (n + m) -> Type) (p : Fin.t n) HL HR :
   case_L_R' P (Fin.L m p) HL HR = HL p.
 Proof.
@@ -239,6 +270,7 @@ Proof.
   - now rewrite IH.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma case_L_R'_R {n m : nat} (P : Fin.t (n + m) -> Type) (p : Fin.t m) HL HR :
   case_L_R' P (Fin.R n p) HL HR = HR p.
 Proof.
@@ -247,24 +279,28 @@ Proof.
   - now rewrite IH.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma case_L_R_L (P : forall n m, t (n + m) -> Type) {n m} (p : Fin.t n) HL HR :
   case_L_R P (Fin.L m p) HL HR = HL _ _ p.
 Proof.
   apply case_L_R'_L.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma case_L_R_R (P : forall n m, t (n + m) -> Type) {n m} (p : Fin.t m) HL HR :
   case_L_R P (Fin.R n p) HL HR = HR _ _ p.
 Proof.
   apply case_L_R'_R.
 Qed.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Fixpoint depair {m n} (o : t m) (p : t n) : t (m * n) :=
 match o with
   |@F1 m' => L (m' * n) p
   |FS o' => R n (depair o' p)
 end.
 
+#[deprecated(since="9.1", note="Please open an issue if you would like stdlib to keep this definition.")]
 Lemma depair_sanity {m n} (o : t m) (p : t n) :
   proj1_sig (to_nat (depair o p)) = n * (proj1_sig (to_nat o)) + (proj1_sig (to_nat p)).
 Proof.
diff --git a/theories/Vectors/FinFun.v b/theories/Vectors/FinFun.v
index de0b054671..3edf217c62 100644
--- a/theories/Vectors/FinFun.v
+++ b/theories/Vectors/FinFun.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 (** An example of finite type : [Fin.t] *)
-#[local] Set Warnings "-stdlib-vector".
+#[local] Set Warnings "-stdlib-vector,-deprecated".
 Set Implicit Arguments.
 From Stdlib Require Import PeanoNat Compare_dec List Finite Fin Permutation.
 Export Finite. (* compat 9.0 *)
diff --git a/theories/Vectors/Vector.v b/theories/Vectors/Vector.v
index 287cc7f140..8e52e94143 100644
--- a/theories/Vectors/Vector.v
+++ b/theories/Vectors/Vector.v
@@ -80,7 +80,7 @@ Originally from the contribution bit vector by Jean Duprat (ENS Lyon).
 
 Based on contents from Util/VecUtil of the CoLoR contribution *)
 
-#[local] Set Warnings "-stdlib-vector".
+#[local] Set Warnings "-stdlib-vector,-deprecated".
 From Stdlib Require Fin.
 From Stdlib Require VectorDef.
 From Stdlib Require VectorSpec.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 2b8f11fb72..c5eb2ee6a2 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -8,9 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** N.B.: Using this encoding of vectors is discouraged.
-See <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v>. *)
-Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be technically difficult, see <https://github.com/coq/stdlib/blob/master/theories/Vectors/Vector.v>.").
+Attributes deprecated(since="9.1", note="Vector92 will replace Vector in Stdlib for Rocq 9.2. You can Require Import that file directly now.").
+Local Set Warnings "-deprecated,-stdlib-vector".
 
 (** Definitions of Vectors and functions to use them
 
@@ -18,25 +17,35 @@ Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be techni
    Institution: PPS, INRIA 12/2010
 *)
 
-(**
-Names should be "caml name in list.ml" if exists and order of arguments
-have to be the same. complain if you see mistakes ... *)
+From Stdlib Require Import Compat.Fin92 Compat.Vector92 VectorFin.
 
 From Stdlib Require Import Arith_base.
-#[local] Set Warnings "-stdlib-vector".
 From Stdlib Require Vectors.Fin.
 Import EqNotations.
 Local Open Scope nat_scope.
 
-(* Set Universe Polymorphism. *)
-
-(**
-A vector is a list of size n whose elements belong to a set A. *)
-
-#[universes(template)]
-Inductive t A : nat -> Type :=
-  |nil : t A 0
-  |cons : forall (h:A) (n:nat), t A n -> t A (S n).
+Universe u.
+#[deprecated(since="9.1", use=Vector92.vec)]
+Notation t := Vector92.vec (only parsing).
+#[deprecated(since="9.1", use=Vector92.nil)]
+Notation nil := Vector92.nil (only parsing).
+#[deprecated(since="9.1", use=Vector92.cons)]
+Notation cons := Vector92.cons (only parsing).
+#[deprecated(since="9.1", use=Vector92.vec_ind)]
+Notation t_ind := Vector92.vec_ind (only parsing).
+#[deprecated(since="9.1", use=Vector92.vec_rect)]
+Notation t_rect := Vector92.vec_ind (only parsing).
+#[deprecated(since="9.1", use=Vector92.vec_rec)]
+Notation t_rec := Vector92.vec_ind (only parsing).
+#[deprecated(since="9.1", use=Vector92.vec_sind)]
+Notation t_sind := Vector92.vec_sind (only parsing).
+
+Arguments nil : clear implicits.
+Arguments cons : clear implicits.
+Arguments t_ind : clear implicits.
+Arguments t_rect : clear implicits.
+Arguments t_rec : clear implicits.
+Arguments t_sind : clear implicits.
 
 Local Notation "[ ]" := (nil _) (format "[ ]").
 Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
@@ -45,6 +54,7 @@ Section SCHEMES.
 
 (** An induction scheme for non-empty vectors *)
 
+#[deprecated(since="9.1", note="Use small inversions. Elaborator input: let '@cons _ a n' v' := v in ...")]
 Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  (bas: forall a: A, P (a :: []))
  (rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
@@ -60,6 +70,7 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
  end.
 
 (** A vector of length [0] is [nil] *)
+#[deprecated(since="9.1", use=Vector92.inj_0)]
 Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
 match v with
   |[] => H
@@ -67,6 +78,7 @@ match v with
 end.
 
 (** A vector of length [S _] is [cons] *)
+#[deprecated(since="9.1", use=Vector92.inj_S)]
 Definition caseS {A} (P : forall {n}, t A (S n) -> Type)
   (H : forall h {n} t, @P n (h :: t)) {n} (v: t A (S n)) : P v :=
 match v with
@@ -74,6 +86,7 @@ match v with
   |_ => fun devil => False_ind (@IDProp) devil (* subterm !!! *)
 end.
 
+#[deprecated(since="9.1", use=Vector92.inj_S)]
 Definition caseS' {A} {n : nat} (v : t A (S n)) : forall (P : t A (S n) -> Type)
   (H : forall h t, P (h :: t)), P v :=
   match v with
@@ -81,6 +94,7 @@ Definition caseS' {A} {n : nat} (v : t A (S n)) : forall (P : t A (S n) -> Type)
   | _ => fun devil => False_rect (@IDProp) devil
   end.
 
+#[deprecated(since="9.1", use=Vector92.inj_S)]
 (** An induction scheme for 2 vectors of same length *)
 Definition rect2 {A B} (P:forall {n}, t A n -> t B n -> Type)
   (bas : P [] []) (rect : forall {n v1 v2}, P v1 v2 ->
@@ -96,20 +110,40 @@ End SCHEMES.
 
 Section BASES.
 (** The first element of a non empty vector *)
+#[deprecated(since="9.1", use=Vector92.hd)]
 Definition hd {A} := @caseS _ (fun n v => A) (fun h n t => h).
 Global Arguments hd {A} {n} v.
 
+#[deprecated(since="9.1", use=Vector92.hd)]
+Lemma hd_92 [A n] v : @hd A n v = @Vector92.hd A n v.
+Proof. rewrite (inj_S v); reflexivity. Qed.
+
 (** The last element of an non empty vector *)
+#[deprecated(since="9.1", use=Vector92.last)]
 Definition last {A} := @rectS _ (fun _ _ => A) (fun a => a) (fun _ _ _ H => H).
 Global Arguments last {A} {n} v.
 
+#[deprecated(since="9.1", use=Vector92.last)]
+Lemma last_92 [A] n v : @last A n v = @Vector92.last A n v.
+Proof.
+  rewrite (inj_S v); set (Vector92.hd v) as h; set (tl v) as t; clearbody h t; clear v.
+  revert h; induction t; trivial; [].
+  set (_ :: t) as v; cbn [last Vector92.last rectS]; cbv [v]; auto.
+Qed.
+
 (** Build a vector of n{^ th} [a] *)
+#[deprecated(since="9.1", use=Vector92.repeat)]
 Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 
+#[deprecated(since="9.1", use=Vector92.repeat)]
+Lemma const_92 : @const = @repeat.
+Proof. reflexivity. Qed.
+
 (** The [p]{^ th} element of a vector of length [m].
 
 Computational behavior of this function should be the same as
 ocaml function. *)
+#[deprecated(since="9.1", use=getFin)]
 Definition nth {A} :=
   fix nth_fix {n : nat} (v : t A n) {struct v} : Fin.t n -> A :=
     match v with
@@ -121,11 +155,22 @@ Definition nth {A} :=
       end v'
     end.
 
+#[deprecated(since="9.1", use=getFin)]
+Lemma nth_92 A n v i : @nth A n v i = @getFin A n v i.
+Proof. induction i; trivial; try rewrite (inj_S v); cbn; trivial. Qed.
+
 (** An equivalent definition of [nth]. *)
+#[deprecated(since="9.1", use=getLt)]
 Definition nth_order {A} {n} (v: t A n) {p} (H: p < n) :=
 (nth v (Fin.of_nat_lt H)).
 
+Lemma nth_order_92 [A n] v p H : @nth_order A n v p H = @getLt A n v p H.
+Proof. cbv [nth_order getLt]. rewrite nth_92. f_equal.
+(* Fin.of_nat_lt H = of_nat n p H *)
+Admitted.
+
 (** Put [a] at the p{^ th} place of [v] *)
+#[deprecated(since="9.1", use=putFin)]
 Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
   match p with
   | @Fin.F1 k => fun v': t A (S k) => caseS' v' _ (fun h t => a :: t)
@@ -133,22 +178,40 @@ Fixpoint replace {A n} (v : t A n) (p: Fin.t n) (a : A) {struct p}: t A n :=
     (caseS' v' (fun _ => t A (S k)) (fun h t => h :: (replace t p' a)))
   end v.
 
+#[deprecated(since="9.1", use=putFin)]
+Lemma replace_92 A n v i x : @replace A n v i x = @putFin A n v i x.
+Proof. induction i; trivial; try rewrite (inj_S v); cbn; congruence. Qed.
+
 (** Version of replace with [lt] *)
+#[deprecated(since="9.1", use=putLt)]
 Definition replace_order {A n} (v: t A n) {p} (H: p < n) :=
 replace v (Fin.of_nat_lt H).
 
+Lemma replace_order_92 [A n] v p H x : @replace_order A n v p H x = @putLt A n v p H x.
+Proof. cbv [replace_order putLt]. rewrite replace_92. f_equal.
+(* Fin.of_nat_lt H = of_nat n p H *)
+Admitted.
+
 (** Remove the first element of a non empty vector *)
+#[deprecated(since="9.1", use=Vector92.tl)]
 Definition tl {A} := @caseS _ (fun n v => t A n) (fun h n t => t).
 Global Arguments tl {A} {n} v.
 
+#[deprecated(since="9.1", use=Vector92.tl)]
+Lemma tl_92 [A n] v : @tl A n v = @Vector92.tl A n v.
+Proof. rewrite (inj_S v); reflexivity. Qed.
+
 (** Destruct a non empty vector *)
+#[deprecated(since="9.1", note="Use small inversions. Elaborator input: let '@cons _ a n' v' := v in ...")]
 Definition uncons {A} {n : nat} (v : t A (S n)) : A * t A n := (hd v, tl v).
 
 (** Remove last element of a non-empty vector *)
+#[deprecated(since="9.1", note="If you would like stdlib to keep this definition, please open an issue.")]
 Definition shiftout {A} := @rectS _ (fun n _ => t A n) (fun a => [])
   (fun h _ _ H => h :: H).
 Global Arguments shiftout {A} {n} v.
 
+#[deprecated(since="9.1", use=Vector92.snoc)]
 (** Add an element at the end of a vector *)
 Fixpoint shiftin {A} {n:nat} (a : A) (v:t A n) : t A (S n) :=
 match v with
@@ -156,12 +219,18 @@ match v with
   |h :: t => h :: (shiftin a t)
 end.
 
+#[deprecated(since="9.1", use=Vector92.snoc)]
+Lemma shiftin_92 [A n] x v : @shiftin A n x v = @Vector92.snoc A n v x.
+Proof. induction v; cbn; congruence. Qed.
+
 (** Copy last element of a vector *)
+#[deprecated(since="9.1", note="If you would like stdlib to keep this definition, please open an issue.")]
 Definition shiftrepeat {A} := @rectS _ (fun n _ => t A (S (S n)))
   (fun h =>  h :: h :: []) (fun h _ _ H => h :: H).
 Global Arguments shiftrepeat {A} {n} v.
 
 (** Take first [p] elements of a vector *)
+#[deprecated(since="9.1", use=Vector92.firstn)]
 Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p :=
   match p as p return p <= n -> t A p with
   | 0 => fun _ => []
@@ -171,7 +240,27 @@ Fixpoint take {A} {n} (p:nat) (le:p <= n) (v:t A n) : t A p :=
     end
   end le.
 
+#[deprecated(since="9.1", use=Vector92.firstn)]
+Lemma take_92_dep [A n] p le v : existT _ _ (@take A n p le v) = existT _ _ (@Vector92.firstn A n v p).
+Proof.
+  revert dependent p; induction v, p; cbn [Nat.min take firstn]; auto;
+    [pose proof Nat.nle_succ_0 p; contradiction|intros].
+  specialize (IHv _ (le_S_n p n le)); symmetry in IHv; inversion_sigma.
+  rewrite <-IHv2; clear IHv2.
+  apply to_list_inj_dep.
+  rewrite 2 to_list_cons, to_list_eq_rect; trivial.
+Qed.
+
+#[deprecated(since="9.1", use=Vector92.firstn)]
+Lemma take_92 [A n] p le v : @take A n p le v = cast (@Vector92.firstn A n v p) (Nat.min_r _ _ le).
+Proof.
+  pose proof eq_sym (take_92_dep p le v) as Hr; inversion_sigma.
+  rewrite <-Hr2; clear Hr2.
+  apply to_list_inj; rewrite to_list_eq_rect, to_list_cast; trivial.
+Qed.
+
 (** Remove [p] last elements of a vector *)
+#[deprecated(since="9.1", use=Vector92.firstn, note="If you would like stdlib to keep this definition, please open an issue.")]
 Lemma trunc : forall {A} {n} (p:nat), n > p -> t A n
   -> t A (n - p).
 Proof.
@@ -187,15 +276,22 @@ Proof.
 Defined.
 
 (** Concatenation of two vectors *)
+#[deprecated(since="9.1", use=Vector92.app)]
 Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) :=
   match v with
   | [] => w
   | a :: v' => a :: (append v' w)
   end.
 
+#[deprecated(since="9.1", use=Vector92.app)]
+Lemma append_92 {A} l p v w : @append A l p v w = @Vector92.app A l v p w.
+Proof. induction v; cbn; congruence. Qed.
+
+#[deprecated(since="9.1")]
 Infix "++" := append.
 
 (** Split a vector into two parts *)
+#[deprecated(since="9.1", use=Vector92.unapp)]
 Fixpoint splitat {A} (l : nat) {r : nat} :
   t A (l + r) -> t A l * t A r :=
   match l with
@@ -205,9 +301,14 @@ Fixpoint splitat {A} (l : nat) {r : nat} :
     (hd v::v1, v2)
   end.
 
+#[deprecated(since="9.1", use=Vector92.unapp)]
+Lemma splitat_92 {A} l r v : @splitat A l r v = @Vector92.unapp A l r v.
+Proof. induction l; cbn; rewrite <-?IHl, ?hd_92, ?tl_92; trivial. Qed.
+
 (** Two definitions of the tail recursive function that appends two lists but
 reverses the first one *)
 
+#[deprecated(since="9.1", use=Vector92.rev_append, note="If you would like stdlib to keep this definition, please open an issue.")]
 (** This one has the exact expected computational behavior *)
 Fixpoint rev_append_tail {A n p} (v : t A n) (w: t A p)
   : t A (Nat.tail_add n p) :=
@@ -216,19 +317,49 @@ Fixpoint rev_append_tail {A n p} (v : t A n) (w: t A p)
   | a :: v' => rev_append_tail v' (a :: w)
   end.
 
+#[deprecated(since="9.1", use=Vector92.rev_append)]
+Lemma rev_append_tail_92 [A n p] v w : existT _ _ (@rev_append_tail A n p v w) = existT _ _ (@Vector92.rev_append A n p v w).
+Proof.
+  revert dependent p; induction v; intros.
+  { cbv [Vector92.rev_append];
+    apply to_list_inj_dep;
+    rewrite ?to_list_cast, ?to_list_of_list; cbn; rewrite ?IHv; trivial. }
+  { cbn; rewrite IHv.
+    apply to_list_inj_dep; cbv [Vector92.rev_append].
+    rewrite ?to_list_cast, ?to_list_cons, ?to_list_of_list.
+    rewrite !List.rev_append_rev; cbn; rewrite <-!List.app_assoc; trivial. }
+Qed.
+
 Import EqdepFacts.
 
 (** This one has a better type *)
+#[deprecated(since="9.1", use=Vector92.rev_append, note="If you would like stdlib to keep this definition, please open an issue.")]
 Definition rev_append {A n p} (v: t A n) (w: t A p)
   :t A (n + p) :=
   rew (Nat.tail_add_spec n p) in (rev_append_tail v w).
 
+#[deprecated(since="9.1", use=Vector92.rev_append)]
+Lemma rev_append_92 [A n p] v w : @rev_append A n p v w = @Vector92.rev_append A n p v w.
+Proof.
+  apply to_list_inj. cbv [rev_append]. rewrite to_list_eq_rect.
+  pose proof eq_sym (@rev_append_tail_92 A n p v w) as HH; inversion_sigma; rewrite <-HH2.
+  rewrite to_list_eq_rect; trivial.
+Qed.
 (** rev [a₁ ; a₂ ; .. ; an] is [an ; a{n-1} ; .. ; a₁]
 
 Caution : There is a lot of rewrite garbage in this definition *)
+#[deprecated(since="9.1", use=Vector92.rev)]
 Definition rev {A n} (v : t A n) : t A n :=
  rew <- (plus_n_O _) in (rev_append v []).
 
+#[deprecated(since="9.1", use=Vector92.rev)]
+Lemma rev_92 [A n] v : @rev A n v = @Vector92.rev A n v.
+Proof.
+  apply to_list_inj; cbv [rev eq_rect_r]; rewrite to_list_eq_rect.
+  rewrite (@rev_append_92 A n 0 v (nil _)); trivial.
+  rewrite to_list_rev_append, to_list_rev, List.app_nil_r; trivial.
+Qed.
+
 End BASES.
 Local Notation "v [@ p ]" := (nth v p) (at level 1).
 
@@ -236,26 +367,44 @@ Section ITERATORS.
 (** * Here are special non dependent useful instantiation of induction schemes *)
 
 (** Uniform application on the arguments of the vector *)
+#[deprecated(since="9.1", use=Vector92.map)]
 Definition map {A} {B} (f : A -> B) : forall {n} (v:t A n), t B n :=
   fix map_fix {n} (v : t A n) : t B n := match v with
   | [] => []
   | a :: v' => (f a) :: (map_fix v')
   end.
 
+#[deprecated(since="9.1", use=Vector92.map)]
+Lemma map_92 : @map = @Vector92.map.
+Proof. reflexivity. Qed.
+
 (** map2 g [x1 .. xn] [y1 .. yn] = [(g x1 y1) .. (g xn yn)] *)
+#[deprecated(since="9.1", use=Vector92.map2)]
 Definition map2 {A B C} (g:A -> B -> C) :
   forall (n : nat), t A n -> t B n -> t C n :=
 @rect2 _ _ (fun n _ _ => t C n) (nil C) (fun _ _ _ H a b => (g a b) :: H).
 Global Arguments map2 {A B C} g {n} v1 v2.
 
+#[deprecated(since="9.1", use=Vector92.map2)]
+Lemma map2_92 {A B C} f n v w : @map2 A B C f n v w = @Vector92.map2 A B C f n v w.
+Proof.
+  induction v; rewrite (inj_0 w) || rewrite (inj_S w); cbn; f_equal; trivial.
+Qed.
+
 (** fold_left f b [x1 .. xn] = f .. (f (f b x1) x2) .. xn *)
+#[deprecated(since="9.1", use=Vector92.fold_left)]
 Definition fold_left {A B:Type} (f:B->A->B): forall (b:B) {n} (v:t A n), B :=
   fix fold_left_fix (b:B) {n} (v : t A n) : B := match v with
     | [] => b
     | a :: w => (fold_left_fix (f b a) w)
   end.
 
+#[deprecated(since="9.1", use=Vector92.fold_right)]
+Lemma fold_left_92 : @fold_left = @Vector92.fold_left.
+Proof. reflexivity. Qed.
+
 (** fold_right f [x1 .. xn] b = f x1 (f x2 .. (f xn b) .. ) *)
+#[deprecated(since="9.1", use=Vector92.fold_right)]
 Definition fold_right {A B : Type} (f : A->B->B) :=
   fix fold_right_fix {n} (v : t A n) (b:B)
   {struct v} : B :=
@@ -264,13 +413,19 @@ Definition fold_right {A B : Type} (f : A->B->B) :=
     | a :: w => f a (fold_right_fix w b)
   end.
 
+#[deprecated(since="9.1", use=Vector92.fold_right)]
+Lemma fold_right_92 : @fold_right = @Vector92.fold_right.
+Proof. reflexivity. Qed.
+
 (** fold_right2 g c [x1 .. xn] [y1 .. yn] = g x1 y1 (g x2 y2 .. (g xn yn c) .. )
     c is before the vectors to be compliant with "refolding". *)
+#[deprecated(since="9.1", note="Use Vector92.fold_right and Vector92.map2. Please open an issue if you would like stdlib to keep this definition.")]
 Definition fold_right2 {A B C} (g:A -> B -> C -> C) (c: C) :=
 @rect2 _ _ (fun _ _ _ => C) c (fun _ _ _ H a b => g a b H).
 
 
 (** fold_left2 f b [x1 .. xn] [y1 .. yn] = g .. (g (g a x1 y1) x2 y2) .. xn yn *)
+#[deprecated(since="9.1", note="Use Vector92.fold_left and Vector92.map2. Please open an issue if you would like stdlib to keep this definition.")]
 Definition fold_left2 {A B C: Type} (f : A -> B -> C -> A) :=
 fix fold_left2_fix (a : A) {n} (v : t B n) : t C n -> A :=
 match v in t _ n0 return t C n0 -> A with
@@ -281,62 +436,39 @@ end.
 
 End ITERATORS.
 
-Section SCANNING.
-Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
- |Forall_nil: Forall P []
- |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
-#[local]
-Hint Constructors Forall : core.
-
-Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
- |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
- |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
-#[local]
-Hint Constructors Exists : core.
-
-Inductive In {A} (a:A): forall {n}, t A n -> Prop :=
- |In_cons_hd {m} (v: t A m): In a (a::v)
- |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v).
-#[local]
-Hint Constructors In : core.
-
-Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
- |Forall2_nil: Forall2 P [] []
- |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 ->
-    Forall2 P (x1::v1) (x2::v2).
-#[local]
-Hint Constructors Forall2 : core.
-
-Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
- |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2)
- |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2).
-#[local]
-Hint Constructors Exists2 : core.
-
-End SCANNING.
-
-Section VECTORLIST.
-(** * vector <=> list functions *)
+#[deprecated(since="9.1", use=Vector92.Forall)]
+Notation Forall := Vector92.Forall (only parsing).
+
+#[deprecated(since="9.1", use=Vector92.Exists)]
+Notation Exists := Vector92.Exists (only parsing).
 
+#[deprecated(since="9.1", use=Vector92.Forall2)]
+Notation Forall2 := Vector92.Forall2 (only parsing).
+
+#[deprecated(since="9.1", use=Vector92.Exists2)]
+Notation Exists2 := Vector92.Exists2 (only parsing).
+
+#[deprecated(since="9.1", use=Vector92.of_list)]
 Fixpoint of_list {A} (l : list A) : t A (length l) :=
 match l as l' return t A (length l') with
   |Datatypes.nil => []
   |(h :: tail)%list => (h :: (of_list tail))
 end.
 
+#[deprecated(since="9.1", use=Vector92.of_list)]
+Lemma of_list_92 {A} l : @of_list A l = @Vector92.of_list A l.
+Proof. induction l; cbn; f_equal; assumption. Qed.
+
+#[deprecated(since="9.1", use=Vector92.to_list)]
 Definition to_list {A}{n} (v : t A n) : list A :=
 Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.nil.
-End VECTORLIST.
+
+#[deprecated(since="9.1", use=Vector92.of_list)]
+Lemma to_list_92 {A} n v : @to_list A n v = @Vector92.to_list A n v.
+Proof. induction v; cbn; f_equal; assumption. Qed.
 
 Module VectorNotations.
-Declare Scope vector_scope.
-Delimit Scope vector_scope with vector.
-Notation "[ ]" := [] (format "[ ]") : vector_scope.
-Notation "h :: t" := (h :: t) (at level 60, right associativity)
-  : vector_scope.
-Notation "[ x ]" := (x :: []) : vector_scope.
-Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
+Export Vector92.VectorNotations.
+#[deprecated(since="9.1")]
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
-Infix "++" := append : vector_scope.
-Open Scope vector_scope.
 End VectorNotations.
diff --git a/theories/Vectors/VectorEq.v b/theories/Vectors/VectorEq.v
index 223fb0c920..c7cd76f72e 100644
--- a/theories/Vectors/VectorEq.v
+++ b/theories/Vectors/VectorEq.v
@@ -18,7 +18,9 @@ Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be techni
    Institution: PPS, INRIA 07/2012
 *)
 
-#[local] Set Warnings "-stdlib-vector".
+From Stdlib Require Import PeanoNat.
+
+#[local] Set Warnings "-stdlib-vector,-deprecated".
 From Stdlib Require Import VectorDef.
 From Stdlib Require Import VectorSpec.
 Import VectorNotations.
@@ -28,14 +30,12 @@ Section BEQ.
  Variables (A: Type) (A_beq: A -> A -> bool).
  Hypothesis A_eqb_eq: forall x y, A_beq x y = true <-> x = y.
 
- Definition eqb:
-   forall {m n} (v1: t A m) (v2: t A n), bool :=
-   fix fix_beq {m n} v1 v2 :=
+ Fixpoint eqb {m n} (v1: t A m) (v2: t A n) : bool :=
    match v1, v2 with
-     |[], [] => true
-     |_ :: _, [] |[], _ :: _ => false
-     |h1 :: t1, h2 :: t2 => A_beq h1 h2 && fix_beq t1 t2
-   end%bool.
+   | [], [] => true
+   | h1::t1, h2::t2 => A_beq h1 h2 && eqb t1 t2
+   | _, _ => false
+   end.
 
  Lemma eqb_nat_eq: forall m n (v1: t A m) (v2: t A n)
   (Hbeq: eqb v1 v2 = true), m = n.
@@ -67,21 +67,5 @@ Section BEQ.
 
 End BEQ.
 
-Section CAST.
-
- Definition cast: forall {A m} (v: t A m) {n}, m = n -> t A n.
- Proof.
- refine (fix cast {A m} (v: t A m) {struct v} :=
-  match v in t _ m' return forall n, m' = n -> t A n with
-  |[] => fun n => match n with
-    | 0 => fun _ => []
-    | S _ => fun H => False_rect _ _
-  end
-  |h :: w => fun n => match n with
-    | 0 => fun H => False_rect _ _
-    | S n' => fun H => h :: (cast w n' (f_equal pred H))
-  end
- end); discriminate.
- Defined.
-
-End CAST.
+#[deprecated(since="9.1", use=Vector92.cast)]
+Notation cast := Vector92.cast (only parsing).
diff --git a/theories/Vectors/VectorFin.v b/theories/Vectors/VectorFin.v
new file mode 100644
index 0000000000..e37e2d2210
--- /dev/null
+++ b/theories/Vectors/VectorFin.v
@@ -0,0 +1,32 @@
+#[local] Set Universe Polymorphism.
+From Stdlib Require Import Compat.Vector92 Compat.Fin92.
+
+Section UniformElementType.
+Context {A : Type}.
+
+Fixpoint getFin {n : nat} (v : vec A n) {struct v} : fin n -> A :=
+  match v with
+  | nil => fun i => False_rect _ (inj_0 i)
+  | cons a v => fun i =>
+    match i in fin n return vec _ (pred n) -> A with
+    | finO => fun _ => a
+    | finS i => fun v => getFin v i
+    end v
+  end.
+
+Fixpoint putFin {n} (v : vec A n) {struct v} : fin n -> A -> vec A n :=
+  match v with
+  | nil => fun _ _ => nil
+  | cons b v => fun i =>
+    match i in fin n return vec _ (pred n) -> _ -> vec _ n with
+    | finO => fun v a => cons a v
+    | finS i => fun v a => cons b (putFin v i a)
+    end v
+  end.
+
+Definition getLt {n} (v: vec A n) {p} (H: p < n) := getFin v (Fin92.of_nat _ _ H).
+Definition putLt {n} (v: vec A n) {p} (H: p < n) := putFin v (Fin92.of_nat _ _ H).
+End UniformElementType.
+
+Lemma nth_error_to_list [A n] (v : vec A n) i : List.nth_error v (to_nat i) = Some (getFin v i).
+Proof. induction v; [case Fin92.inj_0 | case (Fin92.inj_S i) as [->|[? ->] ] ]; cbn; eauto. Qed.
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 118b9b4115..dbe651a781 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -18,22 +18,25 @@ Attributes warn(cats="stdlib vector", note="Using Vector.t is known to be techni
    Institution: PPS, INRIA 12/2010
 *)
 
-#[local] Set Warnings "-stdlib-vector".
+#[local] Set Warnings "-stdlib-vector,deprecated".
 From Stdlib Require Fin List.
-From Stdlib Require Import VectorDef PeanoNat Eqdep_dec.
+From Stdlib Require Import Vector92 VectorFin VectorDef PeanoNat Eqdep_dec.
 Import VectorNotations EqNotations.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this definition, please open an issue.")]
 Definition cons_inj {A} {a1 a2} {n} {v1 v2 : t A n}
  (eq : a1 :: v1 = a2 :: v2) : a1 = a2 /\ v1 = v2 :=
    match eq in _ = x return caseS _ (fun a2' _ v2' => fun v1' => a1 = a2' /\ v1' = v2') x v1
    with | eq_refl => conj eq_refl eq_refl
    end.
 
+#[deprecated(since="9.1", use=Vector92.inj_0)]
 Lemma nil_spec {A} (v : t A 0) : v = [].
 Proof.
 apply (fun P E => case0 P E v). reflexivity.
 Defined.
 
+#[deprecated(since="9.1", use=Vector92.inj_S)]
 Lemma eta {A} {n} (v : t A (S n)) : v = hd v :: tl v.
 Proof.
 apply (fun P IS => caseS P IS (n := n) v); intros; reflexivity.
@@ -44,23 +47,33 @@ is true for the one that use [lt] *)
 
 (** ** Properties of [nth] and [nth_order] *)
 
+Lemma getFin_inj [A n] (v w : t A n)
+  (H : forall i, VectorFin.getFin v i = VectorFin.getFin w i) : v = w.
+Proof.
+  apply Vector92.to_list_inj, List.nth_error_ext; intros i.
+  case (Nat.ltb_spec i n) as [Hi|].
+  { rewrite <-(Fin92.to_nat_of_nat i n Hi), !VectorFin.nth_error_to_list; auto using f_equal. }
+  { rewrite 2 (proj2 (List.nth_error_None _ _)); rewrite ?Vector92.length_to_list; auto. }
+Qed.
+
+Lemma getFin_inj_iff [A n] (v w : t A n) :
+  (forall i, VectorFin.getFin v i = VectorFin.getFin w i) <-> v = w.
+Proof. split; [apply getFin_inj | intros ->; auto]. Qed.
+
+#[deprecated(since="9.1", use=getFin_inj_iff)]
 Lemma eq_nth_iff A n (v1 v2: t A n):
   (forall p1 p2, p1 = p2 -> v1 [@ p1 ] = v2 [@ p2 ]) <-> v1 = v2.
 Proof.
-split.
-- revert n v1 v2; refine (@rect2 _ _ _ _ _).
-  + reflexivity.
-  + intros n ? ? H ? ? H0. f_equal.
-    * apply (H0 Fin.F1 Fin.F1 eq_refl).
-    * apply H. intros p1 p2 H1;
-        apply (H0 (Fin.FS p1) (Fin.FS p2) (f_equal (@Fin.FS n) H1)).
-- intros; now f_equal.
+  rewrite <-getFin_inj_iff; repeat setoid_rewrite nth_92.
+  split; intros; subst; eauto.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_order_hd A: forall n (v : t A (S n)) (H : 0 < S n),
   nth_order v H = hd v.
 Proof. intros n v H; now rewrite (eta v). Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_order_tl A: forall n k (v : t A (S n)) (H : k < n) (HS : S k < S n),
   nth_order (tl v) H = nth_order v HS.
 Proof.
@@ -71,12 +84,14 @@ intros n; induction n; intros k v H HS.
   now rewrite (Fin.of_nat_ext H (proj2 (Nat.succ_lt_mono _ _) HS)).
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_order_last A: forall n (v: t A (S n)) (H: n < S n),
   nth_order v H = last v.
 Proof.
 unfold nth_order; refine (@rectS _ _ _ _); now simpl.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_order_ext A: forall n k (v : t A n) (H1 H2 : k < n),
   nth_order v H1 = nth_order v H2.
 Proof.
@@ -84,6 +99,7 @@ intros n k v H1 H2; unfold nth_order.
 now rewrite (Fin.of_nat_ext H1 H2).
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_append_L A: forall n m (v : t A n) (w : t A m) p,
   (v ++ w) [@ Fin.L m p] = v [@ p].
 Proof.
@@ -92,12 +108,14 @@ intros n m v w. induction v as [|a n v IH].
 - intros p. now apply (Fin.caseS' p).
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma nth_append_R A: forall n m (v : t A n) (w : t A m) p,
   (v ++ w) [@ Fin.R n p] = w [@ p].
 Proof.
 intros n m v w. now induction v.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma In_nth A: forall n (v : t A n) p,
   In (nth v p) v.
 Proof.
@@ -178,6 +196,7 @@ apply (Fin.rect2 (fun n p1 p2 => forall v a b,
     f_equal; apply IH; intros Heq; apply Hneq; now subst.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma replace_append_L A: forall n m (v : t A n) (w : t A m) p a,
   replace (v ++ w) (Fin.L m p) a = (replace v p a) ++ w.
 Proof.
@@ -188,6 +207,7 @@ intros n m v w p a. induction v as [|b n v IH].
   + intros p'. cbn. apply f_equal, IH.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma replace_append_R A: forall n m (v : t A n) (w : t A m) p a,
   replace (v ++ w) (Fin.R n p) a = v ++ (replace w p a).
 Proof.
@@ -203,6 +223,7 @@ Proof.
 now induction p.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.app_repeat_repeat)]
 Lemma append_const A (a : A) n m : (const a n) ++ (const a m) = const a (n + m).
 Proof.
 induction n as [|n IH].
@@ -212,18 +233,21 @@ Qed.
 
 (** ** Properties of [map] *)
 
+#[deprecated(since="9.1", use=Vector92.map_rev)]
 Lemma map_id A: forall n (v : t A n),
   map (fun x => x) v = v.
 Proof.
 intros n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_map)]
 Lemma map_map A B C: forall (f:A->B) (g:B->C) n (v : t A n),
   map g (map f v) = map (fun x => g (f x)) v.
 Proof.
 intros f g n v; induction v as [|? ? v IHv]; simpl; [ | rewrite IHv ]; auto.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_ext_in)]
 Lemma map_ext_in A B: forall (f g:A->B) n (v : t A n),
   (forall a, In a v -> f a = g a) -> map f v = map g v.
 Proof.
@@ -232,6 +256,7 @@ intros f g n v H; induction v as [|? ? v IHv].
 - cbn. now f_equal; [|apply IHv; intros ??]; apply H; [left|right].
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_ext)]
 Lemma map_ext A B: forall (f g:A->B), (forall a, f a = g a) ->
   forall n (v : t A n), map f v = map g v.
 Proof.
@@ -246,6 +271,7 @@ subst p2; induction p1 as [n|n p1 IHp1].
 - revert n v p1 IHp1; refine (@caseS _  _ _); now simpl.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_app)]
 Lemma map_append A B: forall (f:A->B) n m (v: t A n) (w: t A m),
   (map f (v ++ w)) = map f v ++ map f w.
 Proof.
@@ -324,6 +350,7 @@ Qed.
 
 (** ** Properties of [uncons] and [splitat] *)
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
   uncons (a::v) = (a,v).
 Proof. reflexivity. Qed.
@@ -500,6 +527,7 @@ Qed.
 
 (** ** Properties of [shiftin] and [shiftrepeat] *)
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma shiftin_nth A a n (v: t A n) k1 k2 (eq: k1 = k2):
   nth (shiftin a v) (Fin.L_R 1 k1) = nth v k2.
 Proof.
@@ -513,6 +541,7 @@ Proof.
 induction v; now simpl.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma shiftrepeat_nth A: forall n k (v: t A (S n)),
   nth (shiftrepeat v) (Fin.L_R 1 k) = nth v k.
 Proof.
@@ -523,11 +552,13 @@ apply (fun P P0 PS => Fin.rectS P P0 PS k); clear n k.
 - intros n k IH v. rewrite (eta v). apply IH.
 Qed.
 
+#[deprecated(since="9.1", note="If you would like stdlib to keep this lemma, please open an issue.")]
 Lemma shiftrepeat_last A: forall n (v: t A (S n)), last (shiftrepeat v) = last v.
 Proof.
 refine (@rectS _ _ _ _); now simpl.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_snoc)]
 Lemma map_shiftin A B: forall (f : A -> B) a n (v : t A n),
   map f (shiftin a v) = shiftin (f a) (map f v).
 Proof.
@@ -536,6 +567,7 @@ intros f a n v. induction v as [|b n v IH].
 - cbn. apply f_equal, IH.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.fold_right_snoc)]
 Lemma fold_right_shiftin A B: forall (f : A -> B -> B) a b n (v : t A n),
   fold_right f (shiftin b v) a = fold_right f v (f b a).
 Proof.
@@ -562,12 +594,14 @@ Qed.
 
 (** ** Properties of [rev] *)
 
+#[deprecated(since="9.1", use=Vector92.rev_nil)]
 Lemma rev_nil A: rev (nil A) = [].
 Proof.
 unfold rev, rev_append.
 now rewrite (UIP_refl_nat _ (plus_n_O 0)), (UIP_refl_nat _ (Nat.tail_add_spec 0 0)).
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.rev_cons)]
 Lemma rev_cons A: forall a n (v : t A n), rev (a :: v) = shiftin a (rev v).
 Proof.
 intros a n v. unfold rev, rev_append, eq_rect_r.
@@ -580,6 +614,7 @@ induction v as [|b n v IH]; intros m w k E1 E2; cbn.
 - apply (IH _ (b :: w)).
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.rev_snoc)]
 Lemma rev_shiftin A: forall a n (v : t A n),
   rev (shiftin a v) = a :: rev v.
 Proof.
@@ -588,6 +623,7 @@ intros a n v. induction v as [|b n v IH]; cbn.
 - now rewrite !rev_cons, IH.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.rev_rev)]
 Lemma rev_rev A: forall n (v : t A n), rev (rev v) = v.
 Proof.
 intros n v. induction v as [|a n v IH].
@@ -595,6 +631,7 @@ intros n v. induction v as [|a n v IH].
 - now rewrite rev_cons, rev_shiftin, IH.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.map_rev)]
 Lemma map_rev A B: forall (f : A -> B) n (v : t A n),
   map f (rev v) = rev (map f v).
 Proof.
@@ -603,6 +640,7 @@ intros f n v. induction v as [|a n v IH]; cbn.
 - now rewrite !rev_cons, map_shiftin, IH.
 Qed.
 
+#[deprecated(since="9.1", use=Vector92.fold_right_rev)]
 Lemma fold_left_rev_right A B: forall (f:A->B->B) n (v : t A n) a,
   fold_right f (rev v) a = fold_left (fun x y => f y x) a v.
 Proof.
@@ -629,12 +667,9 @@ Qed.
 
 (** ** Properties of [to_list] *)
 
+#[deprecated(since="9.1", use=to_list_of_list)]
 Lemma to_list_of_list_opp {A} (l: list A): to_list (of_list l) = l.
-Proof.
-induction l.
-- reflexivity.
-- unfold to_list; simpl. now f_equal.
-Qed.
+Proof. rewrite to_list_92, of_list_92; apply to_list_of_list. Qed.
 
 Lemma length_to_list A n (v : t A n): length (to_list v) = n.
 Proof. induction v; cbn; auto. Qed.
@@ -709,12 +744,10 @@ Lemma to_list_tl A n (v : t A (S n)):
   to_list (tl v) = List.tl (to_list v).
 Proof. now rewrite (eta v). Qed.
 
+#[deprecated(since="9.1", use=to_list_app)]
 Lemma to_list_append A n m (v1 : t A n) (v2 : t A m):
   to_list (append v1 v2) = List.app (to_list v1) (to_list v2).
-Proof.
-induction v1; simpl; trivial.
-now rewrite to_list_cons; f_equal.
-Qed.
+Proof. rewrite !to_list_92, append_92, to_list_app; trivial. Qed.
 
 Lemma to_list_rev_append_tail A n m (v1 : t A n) (v2 : t A m):
   to_list (rev_append_tail v1 v2) = List.rev_append (to_list v1) (to_list v2).