proposition: Lemma app_union_distr_l: forall L1 L2 L3, L1 >> L3 U L2 >> L3 == (L1 U L2) >> L3.
proof: Proof. split; intros. - destruct H as [H|H]; apply app_in_inv in H; destruct H as (w1, (w2, (?, (Ha, Hb)))); subst; apply app_in_eq; auto. + left. assumption. + right. assumption. - apply app_in_inv in H. destruct H as (w1, (w2, (?, (Ha, Hb)))); subst. apply union_in_inv in Ha. destruct Ha. + apply union_in_l. auto using app_in_eq. + apply union_in_r. auto using app_in_eq. Qed.
imports: Coq.Lists.List