proposition: Lemma path_tur r r' adom bdom (T: transitive r) (DA: doma r' adom) (DB: domb r' bdom) : (r ∪ r')⁺ ≡ r ∪ (r ⨾ ⦗adom⦘ ∪ r')⁺ ⨾ (⦗bdom⦘ ⨾ r)^?.
proof: Proof. split. rewrite seq_eqv_r, seq_eqv_l. unfold seq, union, clos_refl; intros ? ? P. apply clos_trans_tn1 in P; induction P; desf; eauto 14 using clos_trans; clear P. apply clos_trans_t1n in IHP; induction IHP; intuition; desf; eauto 14 using clos_trans. rewrite inclusion_seq_eqv_r, inclusion_seq_eqv_l. eauto using inclusion_t_r_t with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath