proposition: Lemma drop_zero {A: UU} (l: list A): drop l 0 = l.
proof: Proof. revert l. apply list_ind; trivial. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe