Lemma list_ind_compute_2 (P : list -> UU) (p0 : P nil) (ind : ∏ (x : A) (xs : list), P xs -> P (x :: xs)) (x : A) (xs : list) (f := list_ind P p0 ind) : f (x::xs) = ind x xs (f xs). Proof. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.