proposition: Lemma projective_limit_restr_double S K K' (H1:sub K (psI S)) (H2: sub K' K): projective_limit_restr (H2: sub K' (psI (prl_restr H1))) = projective_limit_restr (sub_trans H2 H1).
proof: Proof. apply: projective_limit_Iv;apply:projective_limit_restr_double_Iv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)