proposition: Lemma eq_in_imset2 (f g : aT -> aT2 -> rT) (D : {pred aT}) (D2 : {pred aT2}) : {in D & D2, f =2 g} -> f @2: (D, D2) = g @2: (D, D2).
proof: Proof. move=> eqfg; apply/setP => y. by apply/imset2P/imset2P=> [] [x x2 Dx Dx2 ->]; exists x x2; rewrite ?eqfg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)