proposition: Lemma drop_full {A: UU} (l: list A): drop l (length 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