proposition: Lemma setXb_sub_gfunctions f x: sub (unionb f) x -> sub (productb f) (gfunctions (domain f) x).
proof: Proof. move=> su t /setXb_P [ft dt hyp]; apply/gfunctions_P2;split => //. move=> a /(range_gP ft) [b bt]->; apply: su. rewrite dt in bt;union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)