proposition: Lemma Law_in s E a b: Law s E -> inc a E -> inc b E -> inc (J (J a b) (VL s a b)) s.
proof: Proof. by move => [ha hb hc] aE bE; apply: (fdomain_pr1 hb); rewrite hc; apply:setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)