proposition: Lemma path_dom_same (E1: r ⊆ (⦗d⦘ ∪ ⦗d'⦘) ⨾ r ⨾ (⦗d⦘ ∪ ⦗d'⦘)) (E2: ⦗d⦘ ⨾ ⦗d'⦘ ⊆ ∅₂) dd (DD: dd = ⦗d⦘ ⨾ r ⨾ ⦗d⦘) de (DE: de = ⦗d⦘ ⨾ r ⨾ ⦗d'⦘) ed (ED: ed = ⦗d'⦘ ⨾ r ⨾ ⦗d⦘) ee (EE: ee = ⦗d'⦘ ⨾ r ⨾ ⦗d'⦘) : ⦗d⦘ ⨾ r⁺ ⨾ ⦗d⦘ ⊆ dd⁺ ∪ (dd＊ ⨾ de ⨾ ee＊ ⨾ ed)⁺ ⨾ dd＊.
proof: Proof. rewrite path_dom; try edone. relsf; repeat apply inclusion_union_l; rewrite ?seqA. all: try by rewrite inclusion_seq_eqv_l, inclusion_seq_eqv_r; relsf. { by rewrite ct_begin, EE, ?seqA; sin_rewrite E2; relsf. } { rewrite ct_begin at 1; rewrite EE at 1; rewrite ED at 1; rewrite rtE at 1; relsf. rewrite ?seqA. repeat apply inclusion_union_l; rewrite ?seqA. { by sin_rewrite E2; relsf. } rewrite ct_begin, EE, ?seqA; sin_rewrite E2; relsf. } { rewrite rtE at 1; relsf. rewrite rtE at 1; relsf. repeat apply inclusion_union_l; rewrite ?seqA. { rewrite ED, ?seqA; sin_rewrite E2; relsf. } { rewrite ct_begin, EE, ?seqA; sin_rewrite E2; relsf. } rewrite ct_begin at 1; rewrite ?seqA. rewrite rtE at 1; relsf. rewrite ED, ?seqA; sin_rewrite E2; relsf. rewrite ct_begin, EE, ?seqA; sin_rewrite E2; relsf. } rewrite ?seqA. arewrite (⦗d⦘ ⨾ (dd ＊ ⨾ de ⨾ ee ＊ ⨾ ed) ＊ ⨾ dd ＊ ⊆ fun _ _ => True). rewrite rtE at 1; relsf. rewrite DE, ?seqA. arewrite (⦗d'⦘ ⨾ ⦗d⦘ ⊆ (fun _ _ : A => False)). { by rewrite seq_eqvC in E2. } relsf. rewrite ct_end at 1; rewrite ?seqA. rewrite EE, ?seqA. arewrite (⦗d'⦘ ⨾ ⦗d⦘ ⊆ (fun _ _ : A => False)). { by rewrite seq_eqvC in E2. } relsf. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid