proposition: Lemma semLiftProd4Size A1 A2 A3 A4 B (f : A1 -> A2 -> A3 -> A4 -> B) (g1 : G A1) (g2 : G A2) (g3 : G A3) (g4 : G A4) s : semProdSize (liftProd4 f g1 g2 g3 g4) s <--> [set b : B | exists a1 a2 a3 a4, semProdSize g1 s a1 /\ semProdSize g2 s a2 /\ semProdSize g3 s a3 /\ semProdSize g4 s a4 /\ f a1 a2 a3 a4 = b].
proof: Proof. split; unfold liftProd4; intros. - repeat match goal with | [ H : semProdSize _ _ _ |- _ ] => try (apply semBindSize in H; destruct H as [? [? ?]]); try (apply semReturnSize in H; subst) end. do 4 eexists. repeat (split; [eassumption|]). assumption. - repeat match goal with | [ H : exists _, _ |- _ ] => destruct H as [? [? ?]] | [ H : and _ _ |- _ ] => destruct H as [? ?] end. repeat (apply semBindSize; eexists; split; [eassumption|]). apply semReturnSize. assumption. Qed.
imports: ZArith List Lia mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool ssrnat seq eqtype) QuickChick(Sets Tactics RandomQC)