proposition: Lemma setIrelR z: (alls z reflexivep) -> reflexivep (intersection z).
proof: Proof. move => alr. case: (emptyset_dichot z). move => -> x; rewrite setI_0 /substrate domain_set0 range_set0. by case /setU2_P => /in_set0. move => nez y ys; apply/(setIrel_P nez) => r rz; apply: (alr _ rz). apply: (substrate_sub (setI_s1 rz) ys). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)