proposition: Lemma prl_dl_slice_p2 x: inc x (projective_limit S) -> inc (prl_dl_slice2 x) (projective_limit prl_dl_systemS').
proof: Proof. move=> xp. move:prl_dl_systemS'_prop => [E_S I_S r_S f_S]. rewrite /prl_dl_slice2;apply/prl_limitP; rewrite I_S E_S r_S f_S; split. - fprops. - by aw. - by move => i iI; rewrite !LgV//; apply: prl_dl_slice_p1. - move => i j leij. move: (arg1_sr leij) (arg2_sr leij); rewrite sr2 => iI jI. move:(prl_dl_slice_p1 xp iI) (prl_dl_slice_p1 xp jI). move:(prl_dl_hlm_fct leij); aw; rewrite !LgV//. rewrite 2! prl_dl_F_lambda_prop. set Fj := projective_limit _; set Fi := projective_limit _. rewrite - prl_dl_hml_invariant; move => [ff sf tf] aFi bFj. have ha: inc (Vf (prl_dl_hlm leij) (prl_dl_slice x j)) Fi by Wtac. move/prl_limitP: (aFi) => [xa xb xc xd]. move/prl_limitP: (ha) => [ya yb yc yd]. apply:fgraph_exten => //; first by rewrite xb yb. move: (prl_dl_S_lambda_prop iI) =>[vE1 vI1 vr1 vf1]. rewrite xb /= => k kI. have hb :=(prl_dl_halm_compat leij). rewrite /prl_dl_hlm. set S1 := prl_dl_S_lambda _; set S2 := prl_dl_S_lambda _. have hc: (prl_same_index S1 S2) by []. rewrite -(prl_map_val_aux2 hc hb kI bFj)/prl_dl_slice /prl_dl_halm_fam !LgV//. move /prl_limitP: xp => [_ _ _]; apply;rewrite Sr. apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)