proposition: Lemma setUf_exten I f f': {inc I, f =1 f'} -> unionf I f = unionf I f'.
proof: Proof. move=> hyp; set_extens t;move/setUf_P=> [z zi tf]; apply/setUf_P; ex_tac. by rewrite -hyp. by rewrite hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)