proposition: Lemma prl_restr_canonical_fun_ev S J (H: sub J (psI S)) x: inc x (projective_limit S) -> Vf (prl_restr_canonical H) x = restr x J.
proof: Proof. move => xs; rewrite /prl_restr_canonical LfV//. apply: (prl_restr_canonical_ax H). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)