fact: Definition imset2 T U V (f : T -> U -> V) A1 A2 := imset (uncurry f) (setX A1 A2).
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)