proposition: Lemma path_tur2 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_t1n in P; induction P; desf; eauto 14 using clos_trans; clear P. apply clos_trans_tn1 in IHP0; induction IHP0; intuition; desf; eauto 14 using clos_trans. rewrite inclusion_seq_eqv_r, inclusion_seq_eqv_l. eauto using inclusion_r_t_t with hahn. Qed.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath