proposition: Lemma union_compat_eq_set : forall s1 s1' s2 s2', eq_set s1 s1' -> eq_set s2 s2' -> eq_set (union s1 s2) (union s1' s2').
proof: Proof. intros s1 s1' s2 s2' s1_eq_s1' s2_eq_s2' e; split; intro H. generalize (union_12 s1 s2 e H); intros [e_in_s1 | e_in_s2]. apply union_1; generalize (s1_eq_s1' e); intuition. apply union_2; generalize (s2_eq_s2' e); intuition. generalize (union_12 s1' s2' e H); intros [e_in_s1' | e_in_s2']. apply union_1; generalize (s1_eq_s1' e); intuition. apply union_2; generalize (s2_eq_s2' e); intuition. Qed.
imports: List more_list list_permut Arith