proposition: Lemma LocInObjSet_empty: forall loc, ~ LocInObjSet loc ObjSet.empty = true.
proof: Proof. intros. unfold LocInObjSet. destruct loc. auto. generalize ObjSet_empty. intros. intuition. elim H with o. apply ObjSet.mem_2;trivial. generalize ObjSet_empty. intros. intuition. elim H with o. apply ObjSet.mem_2;trivial. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)