proposition: Lemma tarjan_equiv_true : forall {tarjan} `{DS.WF tarjan} x y u, DS.equiv tarjan x y = (true, u) -> {{tarjan}} x y.
proof: Proof. intros T Hwf x y u H . rewrite <- DS.sameclass_equiv. rewrite H; reflexivity. 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)