proposition: Lemma union_in_equiv: forall L1 L2 L3 L4 w, Equiv L1 L3 -> Equiv L2 L4 -> In w (Union L1 L2) -> In w (Union L3 L4).
proof: Proof. intros. destruct H1. - apply H in H1. apply union_in_l. assumption. - apply H0 in H1. apply union_in_r. assumption. Qed.
imports: Coq.Lists.List