proposition: Lemma acyclic_unc X (r r' : relation X) (A : r ⨾ r ≡ ∅₂) (B : r' ⨾ r' ≡ ∅₂) : acyclic (r ∪ r') <-> acyclic (r ⨾ r').
proof: Proof. unfold acyclic. rewrite pathp_unc, !irreflexive_union; ins. rewrite (irreflexive_seqC r), (irreflexive_seqC r'). rewrite seq_rtE_l, seqA, A, !seq_false_r, union_false_r. rewrite seq_rtE_l, seqA, B, !seq_false_r, union_false_r. rewrite (acyclic_rotl r' r); intuition. by red; ins; eapply A; vauto. by red; ins; eapply B; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath