proposition: Theorem merge_commut{A B C} (f: key -> option A -> option B -> option C) (g: key -> option B -> option A -> option C) : (forall k o1 o2, f k o1 o2 = g k o2 o1) -> forall m1 m2, merge f m1 m2 = merge g m2 m1.
proof: Proof. intros E m1 m2. unfold merge. apply xmerge_commut. intros k [x1|] [x2|]; trivial. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)