proposition: Lemma is_empty_1 :forall m, Empty m -> is_empty m = true.
proof: Proof. unfold Empty, MapsTo. intros m. case m;auto. intros (k,e) l inlist. absurd (InA eqke (k, e) ((k, e) :: l));auto. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses