proposition: Lemma nonempty_nonterminals' {ls nt} (H : is_valid_nonterminal ls nt) : negb (Nat.eqb (nonterminals_length ls) 0).
proof: Proof. pose proof (nonempty_nonterminals H). destruct (nonterminals_length ls); simpl; try reflexivity; try omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Classes.RelationClasses Coq.Setoids.Setoid Coq.ZArith.ZArith Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.BaseTypes