proposition: Lemma Sequence_rect_compute_nil {X} {P : Sequence X ->UU} (p0 : P nil) (ind : ∏ (s : Sequence X) (x : X), P s -> P (append s x)) : Sequence_rect p0 ind nil = p0.
proof: Proof. intros. try reflexivity. unfold Sequence_rect; simpl. change p0 with (transportf P (idpath nil) p0) at 2. apply (maponpaths (λ e, transportf P e p0)). exact (maponpaths (maponpaths functionToSequence) (iscontr_adjointness _ _ _)). Defined.
imports: UniMath.Combinatorics.FiniteSets UniMath.Combinatorics.Lists UniMath.Combinatorics.Vectors UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Tactics