proposition: Lemma state_beq_lb {prestate} {fp : grammar_fixedpoint_lattice_data prestate} (s s' : state) (H : s = s') : s =b s'.
proof: Proof. subst; reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Common Fiat.Common.Wf Fiat.Common.BoolFacts