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