fact: Fixpoint merge (partial_res l : list (A*B)) {struct l} : option (list (A*B)) := match l with | nil => Some partial_res | ((a,b) as p) :: l => match find a partial_res with | Some b' => if eqB_bool b b' then merge partial_res l else None | None => merge (p :: partial_res) l end end.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)