proposition: Lemma prl_r3_F_can_fun: inc prl_r3_F_can (functions (projective_limit S) (projective_limit prl_r3_F)).
proof: Proof. rewrite /prl_r3_F_can;apply/functionsP; saw. apply:lf_function; apply: prl_r3_F_can_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)