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