proposition: Lemma setX1_pr2 f x: domain f = singleton x -> product1 (Vg f x) x = productb f.
proof: Proof. move=> df. rewrite setX1_pr -df (setXb_eq_gfunctions (x:= (Vg f x))) // df. by move => i /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)