proposition: Lemma prod_of_substrates_p g x i: inc x (prod_of_substrates g) -> inc i (domain g) -> inc (Vg x i) (substrate (Vg g i)).
proof: Proof. case/(prod_of_substratesP) => _ _; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)