fact: Definition collapse_lattice_for {T} (l : lattice_for T) : option T := match l with | constant n => Some n | _ => None 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