proposition: Lemma not_mem_not_in : forall a x, LocSet.mem x a = false -> ~ LocSet.In x a.
proof: Proof. intros. intro. apply LocSet.mem_1 in H0. rewrite H0 in H. discriminate H. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical)