proposition: Lemma imset2Ul (A B : {set aT1}) (C : {set aT2}) : f @2: (A :|: B, C) = f @2: (A, C) :|: f @2: (B, C).
proof: Proof. by rewrite !curry_imset2l bigcup_setU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)