proposition: Lemma setIrel_graph z: (alls z sgraph) -> sgraph (intersection z).
proof: Proof. case: (emptyset_dichot z). move => -> _; rewrite setI_0; apply: sgraph_set0. move => [t tz] alg y yi; apply: (alg _ tz); exact: (setI_hi yi tz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)