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