proposition: Lemma rev_shiftin A: forall a n (v : t A n), rev (shiftin a v) = a :: rev v.
proof: Proof. intros a n v. induction v as [|b n v IH]; cbn. - now rewrite rev_cons, !rev_nil. - now rewrite !rev_cons, IH. Qed.
imports: VectorDef PeanoNat Eqdep_dec