proposition: Lemma acyclic_ud r r' adom bdom (A: doma r' adom) (B: domb r' bdom) : acyclic r -> acyclic (⦗bdom⦘ ⨾ r⁺ ⨾ ⦗adom⦘∪ r') -> acyclic (r ∪ r').
proof: Proof. ins; rewrite unionC in *; eauto using acyclic_du. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath