fact: Definition prefix_remove_back {A: decSet} (l1 l2 l3: list A): prefix_remove l1 l2 = just l3 → l2 = l1 ++ l3.
imports: UniMath.Foundations.NaturalNumbers UniMath.Combinatorics.Vectors UniMath.Combinatorics.Lists UniMath.Combinatorics.DecSet UniMath.Combinatorics.Maybe