proposition: Theorem range_domain_exists r: sgraph r -> ((exists! a, forall x, inc x a <-> (exists y, inc (J x y) r)) /\ (exists! b, forall y, inc y b <-> (exists x, inc (J x y) r))).
proof: Proof. move=> gr; split; apply /unique_existence; split. - exists (domain r) => t; apply/(domainP gr). - by move=> x y Hx Hy; set_extens t; rewrite Hx Hy. - by exists (range r) => t; apply/(rangeP gr). - by move=> x y Hx Hy; set_extens t; rewrite Hx Hy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)