proposition: Lemma bindings_Empty m : Empty m <-> bindings m = nil.
proof: Proof. unfold Empty. split; intros H. - assert (H' : forall a, ~ List.In a (bindings m)). { intros (k,e) H'. apply (H k e). rewrite bindings_mapsto_iff, InA_alt. exists (k,e); repeat split; auto with map. } destruct (bindings m) as [|p l]; trivial. destruct (H' p); simpl; auto. - intros x e. rewrite bindings_mapsto_iff, InA_alt. rewrite H. now intros (y,(E,H')). Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)