proposition: Lemma setIt_exten (I:Set) (f f':I-> Set): f =1 f' -> (intersectiont f) = (intersectiont f').
proof: Proof. move=> hyp; case: (emptyset_dichot I) => ie. by rewrite !(setIt_0 _ ie). set_extens t; move/(setIt_P _ ie) => h; apply/(setIt_P _ ie) => j. rewrite - hyp; apply: h. rewrite hyp; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)