proposition: Lemma elements_app : forall (s:t elt) acc, elements_aux acc s = elements s ++ acc.
proof: Proof. induction s; simpl; intros; auto. rewrite IHs1, IHs2. unfold elements; simpl. rewrite 2 IHs1, IHs2, !app_nil_r, <- !app_assoc; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int