proposition: Lemma semLiftProd3Size : forall {A1 A2 A3 B} (f: A1 -> A2 -> A3 -> B) (g1: G A1) (g2: G A2) (g3: G A3) size, semProdSize (liftM3 f g1 g2 g3) size <--> fun b => exists a1, semProdSize g1 size a1 /\ (exists a2, semProdSize g2 size a2 /\ (exists a3, semProdSize g3 size a3 /\ (f a1 a2 a3) = b)).
proof: Proof. solveLiftProdX. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)