proposition: Lemma eq_empty_of_not_binds : forall (A B : Type) (M : map A B), (forall x k, ~ binds M x k) -> M = \{}.
proof: Proof. Proof using. intros A B M. simpl. unfold empty_impl, binds_impl. intros H. apply fun_ext_1. intros x. cases (M x); auto_false*. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)