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