fact: Fixpoint ocons (a: A) (l: list A) {struct l}: list A := match l with nil => a :: nil | b :: l1 => match weight a b with lt => a :: l | eq => a :: l | gt => b :: ocons a l1 end end.
imports: List Permutation UList