proposition: Lemma theta_rho: forall p i, rho p i -> StateSet.Equal (theta i) p.
proof: Proof. intros p i Hpi. assert (Hi := i_table_wf invariant_build_store Hpi). apply proj2, rho_theta in Hi. eapply i_table_inj; eauto. apply invariant_build_store. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)