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