proposition: Lemma path_ur2 r r' adom bdom (A: doma r adom) (B: domb r bdom) : (r ∪ r')⁺ ≡ r'⁺ ∪ (r'⁺ ⨾ ⦗adom⦘)^? ⨾ (r ∪ ⦗bdom⦘ ⨾ r'⁺)⁺.
proof: Proof. ins; rewrite <- path_tur2, ct_of_union_ct_r; eauto; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath