proposition: Lemma olexp'_osr: order_on olexp' (gfunctions (substrate r') (substrate r)).
proof: Proof. move:(olex_osr (olexp_ax)); congr (order_on _ _). rewrite /prod_of_substrates /fam_of_substrates. rewrite - cst_graph_pr /olexp_g /cst_graph; aw;apply: f_equal. apply: Lg_exten => // i isr; rewrite LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)