proposition: Lemma prl_subsets_prop S M (H:prl_subfam_hyp S M) : projective_system_on (projective_system_subsets H) M (psI S) (psr S) (prl_subfam_fct S M).
proof: Proof. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)