proposition: Lemma xbindings_alt m j l : xbindings m j l = List.map (fstmap (rev_append j)) (bindings m) ++ l.
proof: Proof. revert j l. induction m; simpl; intros; auto. destruct o; unfold bindings; simpl; rewrite !IHm1, !IHm2, map_app, map_map, <- app_assoc, app_nil_r; simpl; f_equal; try (apply map_ext; now intros (?,?)); f_equal. - f_equal. rewrite map_map. apply map_ext. now intros (?,?). - rewrite map_map. apply map_ext. now intros (?,?). Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)