{aⁿbⁿcⁿ | n ≥ 1} is not context-free

The positive witness lang_eq_eq_pos differs from lang_eq_eq = {aⁿbⁿcⁿ} only by the empty word, so if it were context-free then lang_eq_eq = lang_eq_eq_pos ∪ {ε} would be too — contradicting notCF_lang_eq_eq.

theorem notCF_lang_eq_eq_pos : ¬is_CF lang_eq_eq_pos