proposition: Lemma theta_below: forall u i, StateSet.In u (theta i) -> i < size' /\ u < size.
proof: Proof. intros u i. unfold theta. apply StateSetMapProps.fold_rec_nodep. StateSetProps.setdec. intros p j q Hpj IH. num_analyse; auto. subst. split. eapply invariant_build_store, Hpj. apply invariant_build_store in Hpj. apply Hpj. assumption. 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)