proposition: Lemma Sprod_case_l2 s E x (f := (s \cg (Sprod (GE_I E) s)) \cg (GE_J E)): Law s E -> (inc x f <-> exists a b c, [/\ inc a E, inc b E, inc c E & x = J (J (J a b) c) (VL s a (VL s b c)) ]).
proof: Proof. move => ll; move: (ll)=> [sE _ _]. split. move /(Sprod_case4 _ sE) => [a [b [c [d [t [ha hb hc]]]]]]. exists a,b,c. move: (sE _ hc) => /setXp_P [ /setXp_P [bE cE ] tE]. move: (sE _ hb) => /setXp_P [ /setXp_P [ aE _] dE]. by split => //; rewrite ha (Law_val ll hb) (Law_val ll hc). move => [a [b [c [aE bE cE ->]]]]. apply/(Sprod_case4 _ sE). exists a,b,c, (VL s a (VL s b c)),(VL s b c); split => //. apply: (Law_in ll aE (Law_range ll bE cE)). apply: (Law_in ll bE cE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)