proposition: Lemma semReturnOpt_None (A : Type) : semProdOpt (ret None) <--> @set0 A.
proof: Proof. intros x1; simpl; split; intros Hin. - unfold semProdOpt, somes in *. eapply semReturn in Hin. inv Hin. - inv Hin. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)