proposition: Lemma semElementsSize {A} (l: list A) (def : A) s : semProdSize (elems_ def l) s <--> if l is nil then [set def] else l.
proof: Proof. rewrite semBindSize. setoid_rewrite semReturnSize. rewrite semChooseSize //=. setoid_rewrite nthE. case: l => [|x l] /=. rewrite (eq_bigcupl [set 0]) ?bigcup_set1 // => n. by rewrite leqn0; split=> [/eqP|->]. rewrite -(@reindex_bigcup _ _ _ (nth def (x :: l)) _ (x :: l)) ?coverE //. by rewrite subn1 /= nth_imset. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)