proposition: Lemma semSizedSizeGen A (f:nat->G A)s : semGenSize (sized f) s <--> semGenSize (f s) s.
proof: Proof. by []. Qed.
imports: Coq(String List ZArith Lia) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat eqtype seq) QuickChick(RandomQC RoseTrees Sets Tactics Producer)