proposition: Lemma no_state_gt_top {prestate} {d : grammar_fixedpoint_lattice_data prestate} (s : state) : (⊤ < s) = false.
proof: Proof. destruct s; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Common Fiat.Common.Wf Fiat.Common.BoolFacts