Deterministic Context-Free Languages Are Not Closed Under Substitution

Counterexample idea: if DCFLs were closed under finite-alphabet substitution, then substituting the two singleton Boolean words [false] and [true] by two arbitrary DCFLs would produce their union. This contradicts the established non-closure of DCFLs under union.

theorem DCF_notClosedUnderSubstitution : ¬ClosedUnderSubstitution fun {α : Type} [Fintype α] => is_DCF

Deterministic context-free languages are not closed under substitution.