proposition: Lemma ex1_F_can_ax: lf_axiom ex1_restr_fun (projective_limit S) (projective_limit ex1_F).
proof: Proof. move:ex1_F_prop => [E_F I_F r_F f_F]. move => z zp. move/prl_limitP:(zp) => [fgz dz zv zw]. rewrite /ex1_restr_fun;apply/prl_limitP; split. - fprops. - by aw. - by rewrite E_F;move => i iL; rewrite !LgV//; apply: ex1_F_can_ax1. - rewrite r_F f_F;move => i j lij. have[iL jL] := ex1_prop2 lij. move: (HJm lij) => s1. move: (ex1_prop7 lij) (ex1_F_can_ax1 jL zp) => ra rb. rewrite /ex1_restr_fun/ex1_gij. rewrite LgV// LgV// LgV//; aw. by rewrite LfV// double_restr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)