proposition: Lemma dom_codom_rel_helper (IN : dom_rel r ⊆₁ d) (IN' : codom_rel r ⊆₁ d'): r ≡ ⦗d⦘ ⨾ r ⨾ ⦗d'⦘.
proof: Proof. unfolder in *. basic_solver 7. Qed.
imports: HahnBase HahnSets HahnRelationsBasic HahnEquational HahnRewrite Setoid