proposition: Lemma ex1_F_can_fun: function_prop ex1_F_can (projective_limit S) (projective_limit ex1_F).
proof: Proof. rewrite /ex1_F_can; saw. by apply:lf_function; apply: ex1_F_can_ax. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)