proposition: Lemma LocSet_remove_diff_remove_add: forall x y e, LocSet.In e x -> x \ (y \ {e}) [=] LocSet.add e (x \ y).
proof: Proof. split; intros. case_eq (MP.FM.eq_dec e a); intros. apply LocSet.add_1; trivial. apply LocSet.add_2. apply LocSet.diff_3. apply LocSet.diff_1 in H0; trivial. apply LocSet.diff_2 in H0. intro; elim H0. apply LocSet.remove_2; trivial. case_eq (MP.FM.eq_dec e a); intros. unfold LocDec.eq in e0; subst. apply LocSet.diff_3; trivial. apply LocSet.remove_1; trivial. apply LocSet.add_3 in H0; trivial. apply LocSet.diff_3. apply LocSet.diff_1 in H0; trivial. apply LocSet.diff_2 in H0. intro; elim H0. apply LocSet.remove_3 in H2; 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)