proposition: Lemma mergeL_eqn f l l' acc k k' v v' : mergeL f ((k,v)::l) ((k',v')::l') acc = match K.compare k k' with | Eq => mergeL f l l' (ocons k (f k (Some v) (Some v')) acc) | Lt => mergeL f ((k,v)::l) l' (ocons k' (f k' None (Some v')) acc) | Gt => mergeL f l ((k',v')::l') (ocons k (f k (Some v) None) acc) end.
proof: Proof. reflexivity. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)