Definition Sequence_rect {X} {P : Sequence X ->UU} (p0 : P nil) (ind : ∏ (x : Sequence X) (y : X), P x -> P (append x y)) (x : Sequence X) : P x. Proof. intros. induction x as [n x]. induction n as [|n IH]. - exact (transportf P (nil_unique x) p0). - exact (transportf P (drop_and_append x) (ind (n,,x ∘ dni_lastelement) (x lastelement) (IH (x ∘ dni_lastelement)))). Defined.
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.