proposition: Lemma drop_nil {A: UU} {n: nat}: @drop A [] n = [].
proof: Proof. induction n ; apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe