proposition: Lemma ObjSet_empty: forall l, ~ ObjSet.In l ObjSet.empty.
proof: Proof. generalize ObjSet.empty_1. intros. unfold ObjSet.Empty in H. apply H. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)