Lemma list_ind : ∏ (P : list -> UU), P nil -> (∏ (x : A) (xs : list), P xs -> P (x :: xs)) -> ∏ xs, P xs. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.StandardFiniteSets. Require Import UniMath.Combinatorics.Vectors.