proposition: Lemma prl_restr_canonical_ax S J (H: sub J (psI S)) : lf_axiom (restr^~J) (projective_limit S) (projective_limit_restr H).
proof: Proof. move => x /Zo_P [hc hd]. apply /prl_limitP;split; aw; fprops. move => i /= iK; rewrite !LgV//; move/setXb_P: hc => [_ _]; apply. by rewrite ps_domain_E; apply:H. move => i j /= ra. by move/setI2_P: (ra) => [rb /setXp_P [iK jK]]; rewrite !LgV//; apply:hd. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)