proposition: Lemma is_empty_1 : Empty m -> is_empty m = true.
proof: Proof. induction m; simpl; auto. rewrite Empty_Node. intros (H,(H0,H1)). subst; simpl. rewrite IHt0_1; simpl; auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface