proposition: Lemma semSized_alt A (f : nat -> G A) `{H : forall n, SizeMonotonic (f n)} (H' : forall n m s, (n <= m)%coq_nat -> semProdSize (f n) s \subset semProdSize (f m) s) : semProd (sized f) <--> \bigcup_n (semProd (f n)).
proof: Proof. rewrite semSized. move => x; split. - move => [n [HT Hs]]. eexists. split; eauto. eexists; eauto. - move => [n [HT [m [_ Hs]]]]. eapply semSized. eexists (m + n). split; [ constructor |]. apply semSizedSize. eapply (H' n). ssromega. eapply (H n); try eassumption. ssromega. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)