proposition: Lemma domainP r: sgraph r -> forall x, (inc x (domain r) <-> (exists y, inc (J x y) r)).
proof: Proof. move=> gr; split; last by move=> [y ]; apply domain_i. by case/funI_P => y yr ->; exists (Q y); rewrite (gr _ yr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)