proposition: Lemma prl_r3_F_can_ax: lf_axiom prl_r3_restr_fun (projective_limit S) (projective_limit prl_r3_F).
proof: Proof. move: prl_r3_F_prop => [E_F I_F r_F f_F]. move => z zp. move/prl_limitP:(zp) => [fgz dz zv zw]. rewrite /prl_r3_restr_fun;apply/prl_limitP; split. - fprops. - by aw. - by rewrite E_F => i iL; rewrite !LgV//; apply: prl_r3_F_can_ax1. - rewrite r_F f_F => i j lij. move/sub_gleP:(lij) => [iL jL s1]. move: (prl_r3_prop7 lij) (prl_r3_F_can_ax1 jL zp) => ra rb. by rewrite /prl_r3_gij !LgV // pr1_pair pr2_pair LfV// double_restr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)