proposition: Lemma prod_related_monotonic {related0_monotonic : forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prerelated0 v s0 -> lattice_for_related prerelated0 v s1} {related1_monotonic : forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prerelated1 v s0 -> lattice_for_related prerelated1 v s1} : forall s0 s1, (s0 <= s1)%fixedpoint -> forall v, lattice_for_related prod_prerelated v s0 -> lattice_for_related prod_prerelated v s1.
proof: Proof. pose proof (fun v => related0_monotonic ⊥%fixedpoint v (bottom_bottom v)). pose proof (fun v => related1_monotonic ⊥%fixedpoint v (bottom_bottom v)). unfold state; simpl in *. 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