proposition: Lemma Law_range s E a b: Law s E -> inc a E -> inc b E -> inc (VL s a b) E.
proof: Proof. move => [ha hb hc] aE bE; rewrite /VL. have pdf: inc (J a b) (domain s) by rewrite hc; apply:setXp_i. by move: (inc_V_range hb pdf) => /funI_P [z /ha /setX_P [ _ _ qb] ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)