proposition: Lemma semThunkGen {A} (f : unit -> G A) : semProd (thunkGen f) <--> semProd (f tt).
proof: Proof. split; intros [r Hr]; exists r; simpl in *; assumption. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)