proposition: Lemma acyclic_union_singl A (r : relation A) a b : acyclic (r ∪ singl_rel a b) <-> acyclic r /\ ~ r＊ b a.
proof: Proof. unfold acyclic; rewrite ct_union_singl, irreflexive_union. rewrite irreflexive_seqC, seqA; rels; intuition; unfolder in *; ins; desf; eauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath