{aⁿbᵐcᵐ} is context-free

The language lang_any_eq = {aⁿbᵐcᵐ | n,m ∈ ℕ} is context-free, presented as the concatenation of {aⁿ} with {bᵐcᵐ}. The latter factor is obtained from lang_aux_ab = {aⁿbⁿ} (proved context-free in Langlib.Classes.ContextFree.Examples.AnBnCm) by a letter permutation.

theorem CF_lang_any_eq : is_CF lang_any_eq