proposition: Lemma IntersectEqual: forall a b a' b', LocSet.Equal a b -> LocSet.Equal a' b' -> LocSet.Equal (LocSet.inter a a') (LocSet.inter b b').
proof: Proof. split; intros. apply LocSet.inter_3. apply LocSet.inter_1 in H1. destruct H with a0; auto. apply LocSet.inter_2 in H1. destruct H0 with a0; auto. apply LocSet.inter_3. apply LocSet.inter_1 in H1. destruct H with a0; auto. apply LocSet.inter_2 in H1. destruct H0 with a0; auto. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)