proposition: Lemma orsum_pr0: forall i, inc i (substrate r) -> exists2 y, inc y (Vg (fam_of_substrates g) i) & inc (J y i) (sum_of_substrates g).
proof: Proof. move=> i idg. move: oa => [or sr alo]; rewrite sr in idg. move: (oa2 idg) => [j js]; exists j; first by rewrite /fam_of_substrates LgV. by apply: disjoint_union_pi1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)