fact: Definition prod_precombine_production_nondep (precombine_production0 : T0 -> T0 -> lattice_for T0) (precombine_production1 : T1 -> T1 -> lattice_for T1) : (lattice_for T0 * lattice_for T1) -> (lattice_for T0 * lattice_for T1) -> lattice_for (lattice_for T0 * lattice_for T1) := fun x y => constant (lattice_for_combine_production precombine_production0 (fst x) (fst y), lattice_for_combine_production precombine_production1 (snd x) (snd y)).
imports: Coq.Sets.Ensembles Fiat.Parsers.StringLike.Core Fiat.Parsers.StringLike.Properties Fiat.Parsers.ContextFreeGrammar.Fix.Properties Fiat.Parsers.ContextFreeGrammar.Fix.Prod Fiat.Parsers.ContextFreeGrammar.Fix.FromAbstractInterpretationDefinitions Fiat.Common Fiat.Common.Instances Fiat.Common.BoolFacts