fact: Definition prefix_remove {A: decSet} (l1 l2: list A): maybe (list A).
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe