proposition: Lemma bindings_app : forall (s:t elt) acc, bindings_aux acc s = bindings s ++ acc.
proof: Proof. induction s; simpl; intros; auto. rewrite IHs1, IHs2. unfold bindings; simpl. rewrite 2 IHs1, IHs2, !app_nil_r, <- !app_assoc; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)