proposition: Lemma curry_codom2l T U V (f : T -> U -> V) : codom (uncurry f) <--> \bigcup_x1 codom (f x1).
proof: Proof. rewrite -imsetT -setXT -/(imset2 f _ _) curry_imset2l. by apply: eq_bigcupr => x; rewrite imsetT. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)