proposition: Lemma dom_eqv1 : dom_rel (⦗d⦘ ⨾ r) ≡₁ d ∩₁ dom_rel r.
proof: Proof. unfold dom_rel, eqv_rel, seq, set_inter, set_equiv, set_subset. split; ins; desf; eauto. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid