fact: Record grammar_fixedpoint_lattice_data_relation {xT yT} (x : grammar_fixedpoint_lattice_data xT) (y : grammar_fixedpoint_lattice_data yT) := { state_relation :> @state _ x -> @state _ y -> Prop; top_state_related : state_relation ⊤ ⊤; state_relation_Proper : Proper (state_beq ==> state_beq ==> iff) state_relation }.
imports: Coq.PArith.BinPos Coq.PArith.Pnat Coq.Arith.Arith Coq.Classes.RelationClasses Coq.Classes.Morphisms Fiat.Parsers.ContextFreeGrammar.Carriers Fiat.Common.Tactics.SplitInContext Fiat.Common.Notations