proposition: Lemma semOneofSize {A} (l : list (G A)) (def : G A) s : semProdSize (oneOf_ def l) s <--> if l is nil then semProdSize def s else \bigcup_(x in l) semProdSize x s.
proof: Proof. case: l => [|g l]. rewrite semBindSize semChooseSize //. rewrite (eq_bigcupl [set 0]) ?bigcup_set1 // => a; split=> [/andP [? ?]|<-] //. by apply/antisym/andP. rewrite semBindSize semChooseSize //. set X := (fun a : nat => is_true (_ && _)). by rewrite (reindex_bigcup (nth def (g :: l)) X) // /X subn1 nth_imset. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)