proposition: Lemma setXb_exten f x x': inc x (productb f) -> inc x' (productb f) -> {inc (domain f), x =1g x'} -> x = x'.
proof: Proof. move=> /setXb_P [fx dx px] /setXb_P [fx' dx' px'] sv. apply: fgraph_exten=>//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)