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