proposition: Lemma T_finaux : forall x y, (x =T= y) = true -> StateSet.mem x (finaux A) = StateSet.mem y (finaux A).
proof: Proof. intros. rewrite T_true in H. destruct tarjan_correct as [_ H']. apply i_final, H. 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(Utils_WF) Coq(Relations) Coq(List)