proposition: Lemma unsized_alt_def : forall A (g : G A) `{@Unsized _ _ PG g}, forall s, semProdSize g s <--> semProd g.
proof: Proof. move => A f H s a. split. move => H'. exists s. split; auto => //. move => [s' [_ H']]. eapply unsized; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)