proposition: Lemma semOneof {A} (l : list (G A)) (def : G A) : semProd (oneOf_ def l) <--> if l is nil then semProd def else \bigcup_(x in l) semProd x.
proof: Proof. by case: l => [|g l]; rewrite 1?bigcupC; apply: eq_bigcupr => sz; apply: semOneofSize. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)