proposition: Lemma setIf_exten I f f': {inc I, f =1 f'} -> intersectionf I f = intersectionf I f'.
proof: Proof. move=> sv; case: (emptyset_dichot I) => ine. by rewrite ine !setIf_0. set_extens t => /(setIf_P _ ine) h;apply/(setIf_P _ ine) => j jI. - by rewrite - (sv _ jI); apply: h. - by rewrite (sv _ jI); apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)