proposition: Lemma fold_right_union: forall e l, LocSet.In e (fold_right LocSet.union LocSet.empty l) <-> exists s, In s l /\ LocSet.In e s.
proof: Proof. induction l. intuition. simpl in H. apply LocSet.empty_1 in H. tauto. destruct H. tauto. simpl. intuition. apply LocSet.union_1 in H1. destruct H1. exists a. split; tauto. apply H in H1. destruct H1. exists x. split; tauto. destruct H1. destruct H1. destruct H1. apply LocSet.union_2. rewrite H1. trivial. apply LocSet.union_3. apply H0. exists x. tauto. 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)