proposition: Lemma prod_on_terminal_correct (on_terminal0 : (Char -> bool) -> lattice_for T0) (on_terminal1 : (Char -> bool) -> lattice_for T1) (on_terminal0_correct : forall P, lattice_for_related prerelated0 (ensemble_on_terminal P) (on_terminal0 P)) (on_terminal1_correct : forall P, lattice_for_related prerelated1 (ensemble_on_terminal P) (on_terminal1 P)) : forall P, lattice_for_related prod_prerelated (ensemble_on_terminal P) (prod_on_terminal on_terminal0 on_terminal1 P).
proof: Proof. t. Qed.
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