proposition: Lemma LocSet_diff_remove_diff_add: forall x y e, (x \ y) \ {e} [=] x \ (LocSet.add e y).
proof: Proof. split; intros. apply LocSet.diff_3. apply LocSet.remove_3 in H. apply LocSet.diff_1 in H. trivial. intro. apply LocSet.add_3 in H0. apply LocSet.remove_3 in H. apply LocSet.diff_2 in H. elim H; trivial. intro. unfold LocSet.E.eq in H1. rewrite H1 in H. apply LocSet.remove_1 in H. elim H. trivial. apply LocSet.remove_2. intro. unfold LocSet.E.eq in H0. rewrite H0 in H. apply LocSet.diff_2 in H. elim H. apply LocSet.add_1. trivial. apply LocSet.diff_3. apply LocSet.diff_1 in H. trivial. apply LocSet.diff_2 in H. intro; elim H. apply LocSet.add_2. trivial. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)