proposition: Lemma UnionEqual: forall a b a' b', ObjSet.Equal a b -> ObjSet.Equal a' b' -> ObjSet.Equal (ObjSet.union a a') (ObjSet.union b b').
proof: Proof. split; intros. apply ObjSet.union_1 in H1;destruct H1. destruct H with a0. apply H2 in H1. apply ObjSet.union_2;trivial. destruct H0 with a0. apply H2 in H1. apply ObjSet.union_3;trivial. apply ObjSet.union_1 in H1;destruct H1. destruct H with a0. apply H3 in H1. apply ObjSet.union_2;trivial. destruct H0 with a0. apply H3 in H1. apply ObjSet.union_3;trivial. Qed.
imports: Coq(List) Coq(Relation_Operators) Coq(DecidableType) Coq(FSetInterface)