proposition: Lemma ex9_can_fun_fp i: inc i I -> function_prop (ex9_can_fun i) (Vg E i) ex9_quo.
proof: Proof. move => iI; rewrite /ex9_can_fun; saw; apply: lf_function. exact:(ex9_can_fun_ax iI). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)