Definition Vector_rect {X : UU} {P : ∏ n, Vector X n -> UU} (p0 : P 0 empty_vec) (ind : ∏ (n : nat) (vec : Vector X n) (x : X), P n vec -> P (S n) (append_vec vec x)) {n : nat} (vec : Vector X n) : P n vec. Proof. intros. induction n as [|n IH]. - refine (transportf (P 0) _ p0). apply proofirrelevancecontr, iscontr_vector_0. - exact (transportf (P _) (drop_and_append_vec vec) (ind _ (vec ∘ dni_lastelement) (vec lastelement) (IH (vec ∘ dni_lastelement)))). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.