proposition: Lemma semLiftProd2Unsized2 {A1 A2 B} (f: A1 -> A2 -> B) (g1 : G A1) (g2 : G A2) `{@Unsized _ _ PG g2}: semProd (liftM2 f g1 g2) <--> f @2: (semProd g1, semProd g2).
proof: Proof. rewrite /semProd. setoid_rewrite semLiftProd2Size. move=> b. split. - move => [n [_ [[a1 a2] [[/= H2 H3] H4]]]]. exists (a1, a2). split; auto; split; eexists; split; eauto; reflexivity. - move => [[a1 a2] [[[s1 /= [H2 H2']] [s2 [H3 H3']]] H4]]. eexists. split; first by auto. exists (a1, a2). split; eauto. split; first by eauto. simpl. eapply unsized; eauto. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)