proposition: Lemma setXf_exten I f x x': inc x (productf I f) -> inc x' (productf I f) -> {inc I, x =1g x'} -> x = x'.
proof: Proof. by move => pa pb pc; apply: (setXb_exten pa pb); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)