proposition: Lemma of_list_1 : forall l x, In x (of_list l) <-> InA E.eq x l.
proof: Proof. induction l; simpl; intro x. - rewrite empty_iff, InA_nil. intuition. - rewrite add_iff, InA_cons, IHl. intuition. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide