proposition: Lemma prl_restr_prop S J (H: sub J (psI S)): projective_system_on (prl_restr H) (restr (psE S) J) J (induced_order (psr S) J) (restr (psf S) (induced_order (psr S) J)).
proof: Proof. done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)