proposition: Lemma olex_Fe: (substrate r' = emptyset) -> singletonp olexp_G.
proof: Proof. move => h; exists emptyset; apply: set1_pr. apply: Zo_i. apply /gfunctions_P1;split;fprops. apply fgraph_set0. by rewrite domain_set0. suff: (olexp_I emptyset = emptyset) by move => ->; apply: emptyset_finite. by apply/set0_P => t /Zo_P; rewrite h; move=> [/in_set0]. by move => z /Zo_P [] /gfunctions_P1 [_]; rewrite h;move /domain_set0_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)