proposition: Lemma prl_dl3_res (X := (projective_limit prl_dl3_systemS)) (Y := projective_limit prl_dl3_systemS'): bijection_prop (Lf prl_dl3_mod X Y) X Y.
proof: Proof. saw; apply: lf_bijective. + move => x xX; move/setXb_P:( prl_dl3_mod_p1 xX)=> []; aw => pa pb pc. apply/prl_limitP; split; fprops => i j /= lij. move:(arg1_sr lij)(arg2_sr lij); rewrite sr => iI jI. rewrite /prl_dl3_mod / prl_dl3_ffam LgV// LgV// LgV//. move/prl_limitP: xX => [qa qb qc qd]. rewrite (ext_map_prod_V (prl_dl3_ffam_ax lij)). apply:Lg_exten => l lL; rewrite/ext_map_prod_aux -/(Vf _ _). have ha:gle prl_dl3_or (J i l) (J j l). by apply/pidl_gleP; split; aww;apply/diagonal_pi_P. by rewrite (qd _ _ ha) /= /prl_dl3_f; rewrite ! LgV//; aw. apply/setXf_P; split;aww => l lL; rewrite LgV//. have ha:= (setXp_i jI lL). by move: (qc (J j l) ha); rewrite /= /prl_dl3_E LgV//; aw. + apply prl_dl3_mod_inj. + move => y /prl_limitP[] /= fgy dy pa pb. set x := Lg (I\times L) (fun il => Vg (Vg y (P il)) (Q il)). exists x. rewrite /x;apply/prl_limitP; split; aww. move => il /= ilIL; rewrite LgV//. move/setX_P: (ilIL) => [pp iI lL]; move:(pa _ iI); rewrite LgV//. rewrite /prl_dl3_E /prl_dl3_Ep LgV//. move/setXb_P => [qa qb ]; aw; rewrite /prl_dl3_Efam; aw => qc. move: (qc _ lL); rewrite LgV//. move => p1 p2 /= lp1p2. move: (prl_dl3_or_prop1 lp1p2); aw; move => [_ p1p p2p l12 qq]. have hq: inc (Q p1) L by case/setX_P:p1p. move:(pb _ _ l12); rewrite /prl_dl3_f /prl_dl3_ffam !LgV//; aw. rewrite (ext_map_prod_V). by move => ->; rewrite /ext_map_prod_aux LgV// qq. by move:(prl_dl3_ffam_ax l12); aw. have hr: inc (P p2) I by case/setX_P:p2p. move:(pa _ hr); rewrite LgV//. rewrite/x/prl_dl3_mod;apply: fgraph_exten; aww. rewrite dy;move => i iI /=; rewrite LgV//. move: (pa _ iI); rewrite LgV// => /setXb_P[]. rewrite /prl_dl3_Efam;aw => qa qb qc. apply:fgraph_exten; aww; rewrite qb => l lL. have ha: inc (J i l) (I \times L) by apply: setXp_i. by rewrite ! LgV//; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)