proposition: Lemma ex1_F_can_ax1 i z: inc i L -> inc z (projective_limit S) -> inc (restr z (Vg Jf i)) (ex1_Fl i).
proof: Proof. move => iL zp; move:(prl_restr_canonical_ax(ex1_prop4 iL) zp). by congr inc; apply:projective_limit_Iv; apply:ex1_prop5b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)