proposition: Lemma path_utd_helper : forall X (r r' : relation X) (T: transitive r') dom (F: is_total dom r') (DA: doma r' dom) (DB: domb r' dom) x y (P: clos_trans (fun x y => r x y \/ r' x y) x y), r⁺ x y \/ (exists z w, r＊ x z /\ r' z w /\ r＊ w y) \/ (exists z w, r' z w /\ r＊ w z).
proof: Proof. ins; induction P; desf; eauto 9 using clos_trans, clos_refl_trans, clos_trans_in_rt. right; destruct (classic (z1 = w)) as [|NEQ]; desf; eauto 8 using clos_refl_trans. eapply F in NEQ; desf; eauto 8 using clos_refl_trans. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath