proposition: Lemma drop_step {A: UU} (x: A) (xs: list A) (n: nat) : drop (x :: xs) (S n) = drop xs n.
proof: Proof. apply idpath. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe