proposition: 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: Proof. apply idpath. Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors