Context-Sensitive Closure Under ε-Free Homomorphism

This file proves that context-sensitive languages are closed under string homomorphisms that do not erase symbols.

theorem CS_closedUnderEpsFreeHomomorphism : ClosedUnderEpsFreeHomomorphism fun {α : Type} [Fintype α] => is_CS

Context-sensitive languages are closed under ε-free string homomorphism.