proposition: 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).
proof: Proof. intros. cbn. Abort. Lemma append_length {X} (x:Sequence X) (y:X) : length (append x y) = S (length x). Proof. intros. reflexivity. Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics