fact: Fixpoint lexico (l1 l2: list A) {struct l1}: cmp := match l1 with nil => match l2 with nil => eq | _ => lt end | a:: l3 => match l2 with nil => gt | b :: l4 => match weight a b with eq => lexico l3 l4 | X => X end end end.
imports: List Permutation UList