proposition: Lemma prl_restr_canonical_fp S J (H: sub J (psI S)): function_prop (prl_restr_canonical H) (projective_limit S) (projective_limit_restr H).
proof: Proof. rewrite /prl_restr_canonical; saw. apply:(lf_function (prl_restr_canonical_ax H)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)