intro w
case h
α : Type u_1
L1 L2 L3 : Language α
⊢ ∀ (x : Word α), x ∈ L1 ∘ₗ (L2 ∪ L3) ↔ x ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ (L2 ∪ L3) ↔ w ∈ L1 ∘ₗ L2 ∪ L1 ∘ₗ L3