proposition: Lemma projective_limit_restr_double_Iv S K K' (H1:sub K (psI S)) (H2: sub K' K): prl_same_data (prl_restr (H2: sub K' (psI (prl_restr H1)))) (prl_restr (sub_trans H2 H1)).
proof: Proof. have ha: restr (restr (psE S) K) K' = restr (psE S) K'. by rewrite double_restr. have hb: induced_order (induced_order (psr S) K) K' = induced_order (psr S) K'. by rewrite (iorder_trans _ H2). split => //=;rewrite double_restr ? hb // => t /setI2_P [qa qb]. by apply/setI2_P; split => //; apply: (setX_Sll H2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)