proposition: Lemma path_utd : forall X (r r' : relation X) (T: transitive r') dom (F: is_total dom r') (DA: doma r' dom) (DB: domb r' dom) (I': irreflexive (r' ⨾ r＊)), (r ∪ r')⁺ ≡ r⁺ ∪ r＊ ⨾ r' ⨾ r＊.
proof: Proof. split. unfold inclusion, seq, union in *; ins; desf. eapply path_utd_helper with (2:=F) in H; desf; eauto 8; exfalso; eauto 8. apply inclusion_union_l; eauto with hahn. rewrite <- rt_ct, ct_begin; eauto with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath