proposition: Lemma simulation: forall i j, (i =T= j) = true -> belong i A -> belong j A -> forall a, a < max_label A -> (delta a i =T= delta a j) = true.
proof: Proof. intros. rewrite T_true in *. destruct tarjan_correct as [[H' _ _ _] _]. eapply (H' nil diag_empty); trivial. 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)