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