proposition: Lemma du_index_pr1 g x: inc x (sum_of_substrates g) -> [/\ inc (Q x) (domain g), inc (P x) (substrate (Vg g (Q x))) & pairp x].
proof: Proof. move=> xdu; move :(disjointU_hi xdu) => []. rewrite fos_d => h; rewrite LgV// => h1; split. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)