constructor
case h
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 ↔ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3
case h.mp
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ (L1 ∪ L2) ∘ₗ L3 → w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3

case h.mpr
α : Type u_1
L1 L2 L3 : Language α
w : Word α
⊢ w ∈ L1 ∘ₗ L3 ∪ L2 ∘ₗ L3 → w ∈ (L1 ∪ L2) ∘ₗ L3