proposition: Lemma semReturnSizeOpt (A : Type) (x : A) (size : nat) : semProdSizeOpt (ret (Some x)) size <--> [set x].
proof: Proof. intros x1; simpl; split; intros Hin. - unfold semProdSizeOpt, somes in *. eapply semReturnSize in Hin. inv Hin. reflexivity. - unfold semProdSizeOpt, somes in *. eapply semReturnSize. inv Hin. reflexivity. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)