intro
| ⟨u,v,h1,h2,h3⟩ =>
  cases h2 with
  | inl hl => apply Or.inl; exists u; exists v
  | inr hr => apply Or.inr; exists u; exists v
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) → w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
no goals