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