proposition: Lemma semSequenceProdSize A (gs : list (G A)) n : semProdSize (sequenceProd gs) n <--> [set l | length l = length gs /\ List.Forall2 (fun y => semProdSize y n) gs l].
proof: Proof. elim: gs => [|g gs IHgs]. by rewrite semReturnSize /set1; case=> // a l; split=> // [[]]. rewrite /= semBindSize; setoid_rewrite semBindSize; setoid_rewrite semReturnSize. setoid_rewrite IHgs; case=> [| x l]. split; first by case=> ? [? [? [?]]]. by move=> H; inversion H. rewrite Forall2_cons; split; first by case=> y [gen_y [s [[<- ?]]]] [<- <-]. by case=> [[<-] [? ?]]; exists x; split => //; exists l; split. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)