proposition: Lemma prod_of_substrates_gi g f: (forall i, inc i (domain g) -> inc (f i) (substrate (Vg g i))) -> inc (Lg (domain g) f) (prod_of_substrates g).
proof: Proof. move => pb; apply/(prod_of_substratesP);split => //; aww=> i idg. by rewrite LgV //; apply: pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)