proposition: Lemma immediate_adjacent A (r: relation A) (dom: A -> Prop) (STOT1: ⦗dom⦘ ⨾ r ⨾ r^{-1} ⊆ r^? ∪ r^{-1}) (STOT2: r^{-1} ⨾ ⦗dom⦘ ⨾ r ⊆ r^? ∪ r^{-1}) (T: transitive r) (IRR: irreflexive r): ⦗dom⦘ ⨾ immediate r ≡ ⦗dom⦘ ⨾ (adjacent r ∩ r).
proof: Proof. unfold adjacent; unfolder in *; ins. split; splits; desf; ins; try done. 1, 3: by eauto with hahn. assert (AA: dom x /\ (exists z : A, r x z /\ r c z) ) by eauto. by specialize (STOT1 x c AA) ; desf; [auto|exfalso; eauto |econs]. assert (AA: (exists z : A, r z y /\ dom z /\ r z c) ) by eauto. by specialize (STOT2 y c AA) ; desf; [auto|econs | exfalso; eauto]. apply LA_bc in R1; apply LA_ca in R2; desf; eapply IRR, T; eauto. Qed.
imports: HahnBase HahnRelationsBasic HahnRewrite Setoid