proposition: Lemma trivial_grammar_parses_only_empty_string s : parse_of_grammar s trivial_grammar -> length s = 0.
proof: Proof. intro H; hnf in H; simpl in H. repeat match goal with | _ => reflexivity | _ => assumption | [ H : parse_of _ _ _ |- _ ] => inversion_clear H | [ H : parse_of_production _ _ _ |- _ ] => inversion_clear H end. Qed.
imports: Coq.Strings.String Coq.Lists.List Fiat.Parsers.ContextFreeGrammar.Core Fiat.Parsers.ContextFreeGrammar.PreNotations