proposition: Lemma prl_dl_slice_p1 x lam: inc x (projective_limit S) -> inc lam I2 -> inc (prl_dl_slice x lam) (prl_dl_F_lambda lam).
proof: Proof. move => xl lI;rewrite (prl_dl_F_lambda_prop). move: (prl_dl_S_lambda_prop lI) =>[E_S I_S r_S f_S]. move/prl_limitP: (xl) => [xa xb xc xd]. rewrite /prl_dl_slice; apply/prl_limitP; rewrite I_S E_S r_S f_S; split. - fprops. - by aw. - move => i iI;rewrite /prl_dl_Elam_fam !LgV//; apply: xc. by rewrite prl_dl_I; apply:setXp_i. - move => i j leij;rewrite /prl_dl_Elam_fam. move: (arg1_sr leij) (arg2_sr leij); rewrite sr1 => iI jI. rewrite /prl_dl_glam_fam !LgV//; aw;apply:xd. rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or2); rewrite sr2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)