proposition: Lemma path_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. split. eapply inclusion_rt_ind_left; eauto with hahn. rewrite seq_union_l, !seq_union_r, <- !seqA, <- !ct_begin. rewrite (seq_rtE_r r (r ⨾ r')), (seq_rtE_r r' (r' ⨾ r)), <- !seqA. rewrite A, B, ?seq_false_l, ?union_false_l, ?union_false_r. by unfold union, seq; red; ins; desf; eauto 6 using clos_trans_in_rt, rt_refl. hahn_rel; repeat first [apply inclusion_union_l|apply inclusion_seq_rt| eapply inclusion_rt_rt2]; vauto. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath