proposition: Lemma nonempty_nonterminals {ls nt} (H : is_valid_nonterminal ls nt) : 0 < nonterminals_length ls.
proof: Proof. eapply Nat.le_lt_trans; [ apply Nat.le_0_l | exact (remove_nonterminal_dec ls nt H) ]. 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