proposition: Lemma curry_imset2X : f @2: (A1, A2) = uncurry f @: (setX A1 A2).
proof: Proof. rewrite [@imset]unlock unlock; apply/setP=> x; rewrite !in_set; congr (x \in _). by apply: eq_image => u //=; rewrite !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)