fact: Definition lattice_for_lub {T} (lub : T -> T -> lattice_for T) (x y : lattice_for T) := match x, y with | ⊤, ⊤ => ⊤ | constant x', constant y' => lub x' y' | ⊥, ⊥ => ⊥ | ⊤, _ | _, ⊤ => ⊤ | ⊥, v | v, ⊥ => v end.
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