proposition: Lemma list_ind : ∏ (P : list -> UU), P nil -> (∏ (x : A) (xs : list), P xs -> P (x :: xs)) -> ∏ xs, P xs.
proof: Proof. intros P Hnil Hcons xs. induction xs as [n xs]. induction n as [|n IHn]. - induction xs. apply Hnil. - simpl in xs. induction xs as [x xs]. apply (Hcons x (n,,xs) (IHn xs)). Defined.
imports: UniMath.MoreFoundations.Tactics UniMath.Combinatorics.StandardFiniteSets UniMath.Combinatorics.Vectors