Lemma Sequence_rect_compute_cons {X} {P : Sequence X ->UU} (p0 : P nil) (ind : ∏ (s : Sequence X) (x : X), P s -> P (append s x)) (p := Sequence_rect p0 ind) (x:X) (l:Sequence X) : p (append l x) = ind l x (p l).
Require Import UniMath.Combinatorics.Vectors. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics.