proposition: Lemma prl_r3_F_can_ax1 i z: inc i prl_r3_nI -> inc z (projective_limit S) -> inc (restr z i) (prl_r3_Fl i).
proof: Proof. move => iL zp; move:(prl_restr_canonical_ax(prl_r3_prop4 iL) zp). by congr inc; apply:projective_limit_Iv; apply:prl_r3_prop5b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)