proposition: Lemma semThunkGenSize {A} (f : unit -> G A) s : semProdSize (thunkGen f) s <--> semProdSize (f tt) s.
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)