proposition: Lemma prl_r3_res1 i: inc i prl_r3_nI -> function_prop (prl_r3_gi i) (projective_limit S) (prl_r3_Fl i).
proof: Proof. move => iL;rewrite /prl_r3_gi; rewrite prl_r3_res0; apply:prl_restr_canonical_fp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)