proposition: Theorem xmerge_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 i, xmerge f m1 m2 i = xmerge g m2 m1 i.
proof: Proof. intros E. induction m1; destruct m2; intros i; simpl; trivial; f_equal; try apply IHm1_1; try apply IHm1_2; try apply xmapi_ext; intros; apply E. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)