proposition: Lemma prod_of_substratesP g x: inc x (prod_of_substrates g) <-> [/\ fgraph x, domain x = domain g & forall i, inc i (domain g) -> inc (Vg x i) (substrate (Vg g i))].
proof: Proof. split. move/setXb_P; aw; move=> [fgx dx asu];split => //. by move => i idg; move: (asu _ idg); rewrite LgV. move => [pa pb pc]; apply /setXb_P; aw;split=> // i idg. rewrite LgV //; exact: (pc _ idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)