proposition: Lemma disjoint_union_pi1 g x y: inc y (domain g) -> inc x (substrate (Vg g y)) -> inc (J x y) (sum_of_substrates g).
proof: Proof. by move=> ydg xsv; apply: disjointU_pi; aw; trivial; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)