proposition: Lemma pathp_unc X (r r' : relation X) (A : r ⨾ r ≡ ∅₂) (B : r' ⨾ r' ≡ ∅₂) : (r ∪ r')⁺ ≡ (r ⨾ r')⁺ ∪ (r' ⨾ r)⁺ ∪ r ⨾ (r' ⨾ r)＊ ∪ r' ⨾ (r ⨾ r')＊.
proof: Proof. rewrite ct_begin, path_unc; ins. rewrite seq_union_l, !seq_union_r, <- !seqA, <- !ct_begin. rewrite (seq_rtE_r r (seq r r')), (seq_rtE_r r' (seq r' r)), <- !seqA. rewrite A, B, ?seq_false_l, ?union_false_l, ?union_false_r. by unfold union, seq; split; red; ins; desf; eauto 8 using rt_refl. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath