proposition: Lemma curry_imset2l T U V (f : T -> U -> V) A1 A2 : f @2: (A1, A2) <--> \bigcup_(x1 in A1) f x1 @: A2.
proof: Proof. move=> a; split. by case=> [[x1 x2] [[/= Ax1 Ax2] fx]]; exists x1; split=> //; exists x2. by case=> [x1 [Ax1 [x2 [Ax2 fx]]]]; exists (x1,x2). Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)