proposition: Lemma order_graph_pr1: gfunctions x y = prod_of_substrates (cst_graph x g).
proof: Proof. rewrite -cst_graph_pr /prod_of_substrates /fam_of_substrates /cst_graph. aw; rewrite - sr; congr productb; apply: Lg_exten => v vs; rewrite LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)