proposition: Lemma list2LocSet_1: forall x l, In x l <-> LocSet.In x (list2LocSet l).
proof: Proof. induction l. split; intros. inversion H. unfold list2LocSet in H. generalize LocSet.empty_1. intros. unfold LocSet.Empty in H0. elim H0 with x; trivial. split; intros. simpl in H. destruct H. unfold list2LocSet. apply LocSet.add_1. trivial. destruct IHl. unfold list2LocSet. apply LocSet.add_2. apply H0; trivial. unfold list2LocSet in H. case_eq (LocDec.eq_dec x a); intros. intuition. unfold LocDec.eq in e. rewrite e. auto with *. apply LocSet.add_3 in H. rewrite <- IHl in H. auto with *. auto. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)