proposition: Lemma setI_prop x: intersection x = intersectionf x id.
proof: Proof. case: (emptyset_dichot x) => xe; first by rewrite xe setI_0 setIf_0. set_extens t; first by move/(setI_P xe) =>h; apply:setIf_i. by move/(setIf_P _ xe) =>h;apply:setI_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)