proposition: Lemma Sprod_case2 s E : Law s E -> s \cg (Sprod s (GE_I E)) = fun_image ((E\times E) \times E) (fun z=> J z (VL s (VL s (P (P z)) (Q (P z))) (Q z))).
proof: Proof. move => h. apply:extensionality => x. move /(Sprod_case_l1 _ h) => [a [b [c [aE bE cE]]] ->]. apply/funI_P; exists (J (J a b) c); aw;trivial. by apply:setXp_i => //; apply:setXp_i. move => /funI_P [z /setX_P[pz /setX_P [ppz ha hb] hc] ->]. apply/(Sprod_case_l1 _ h); exists (P (P z)), (Q (P z)), (Q z). by rewrite ppz pz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)