proposition: Lemma epsilon_t_add_one: forall i j A s t, epsilon_t (add_one i j A) s t -> epsilon_t A s t \/ epsilon_rt A s i /\ epsilon_rt A j t.
proof: Proof. induction 1. apply epsilon_add_one in H as [H | [-> ->]]. left. constructor 1. assumption. right. split; constructor 2. intuition. left. econstructor 2; eassumption. right; intuition. eauto using rt_trans, t_rt. right; intuition. eauto using rt_trans, t_rt. 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_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)