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