proposition: Lemma state_le_refl {prestate} {fp : grammar_fixedpoint_lattice_data prestate} (s : state) : s <= s.
proof: Proof. unfold state_le. rewrite state_beq_lb by reflexivity. reflexivity. Qed.
imports: Fiat.Parsers.ContextFreeGrammar.Fix.Definitions Fiat.Common Fiat.Common.Wf Fiat.Common.BoolFacts