proposition: Lemma union_assoc_in_2: forall L1 L2 L3 w, In w (Union (Union L1 L2) L3) -> In w (Union L1 (Union L2 L3)).
proof: Proof. intros. destruct H as [[H|H]|H]. - left; assumption. - right. left. assumption. - right. right. assumption. Qed.
imports: Coq.Lists.List