proposition: Lemma prl_dl_canon_bijection: bijection_prop prl_dl_can_iso (projective_limit S) (projective_limit prl_dl_systemS').
proof: Proof. rewrite /prl_dl_can_iso; saw; apply:lf_bijective. - apply:prl_dl_slice_p2. - move => u v ul vl sv. move /prl_limitP: (ul) => [ua ub uc ud]. move /prl_limitP: (vl) => [va vb vc vd]. apply/fgraph_exten => //; first by rewrite vb. rewrite ub prl_dl_I; move => p /setX_P [pp iI lL]. move:(f_equal (fun z => Vg (Vg z (Q p)) (P p)) sv). by rewrite /prl_dl_slice2 /prl_dl_slice; rewrite !LgV // pp. move => y yl. pose x := Lg (psI S) (fun p => Vg (Vg y (Q p)) (P p)). move/prl_limitP: (yl) => []. move: prl_dl_systemS'_prop => [ES IS rS fS]. rewrite ES IS rS fS => ya yb yc yd. have xa: fgraph x by rewrite /x; fprops. have xb: domain x = psI S by rewrite /x; aw. have xc i:inc i (psI S) -> inc (Vg x i) (Vg (psE S) i). rewrite /x => iI; rewrite LgV//. move: iI; rewrite prl_dl_I => /setX_P [pi i1I i2I]. move:(yc _ i2I); rewrite LgV //prl_dl_F_lambda_prop. move:(prl_dl_S_lambda_prop i2I) => [Esj Isj rsj fsj]. move/ (prl_limitP);rewrite Esj Isj;move => [_ _ yic _]. by move: (yic _ i1I); rewrite /prl_dl_Elam_fam LgV// pi. have xd i j: gle (psr S) i j -> Vg x i = Vf (Vg (psf S) (J i j)) (Vg x j). move => lp1p2; rewrite /x. move:(arg1_sr lp1p2) (arg2_sr lp1p2); rewrite ps_substrate_r => iI jI. rewrite ! LgV//. move: iI jI; rewrite prl_dl_I => /setX_P [pi i1I i2I] /setX_P [pj j1I j2I]. move:lp1p2; rewrite Sr => /pidl_gleP [_ _ leI leL]. rewrite (yd _ _ leL) LgV//-prl_dl_hml_invariant /prl_dl_hlm. move: (yc _ j2I); rewrite LgV// (prl_dl_F_lambda_prop (pidl_i2_L sr2 leL)). set S1 := prl_dl_S_lambda _; set S2 := prl_dl_S_lambda _ => yjp. have ha: prl_same_index S1 S2 by []. have hb :=(prl_dl_halm_compat leL). rewrite - (prl_map_val_aux2 ha hb i1I yjp) /prl_dl_halm_fam LgV//. move: (yc _ j2I);rewrite LgV // prl_dl_F_lambda_prop => /prl_limitP []. move:(prl_dl_S_lambda_prop j2I) => [Esj Isj rsj fsj]. rewrite Esj Isj rsj fsj => yja yjb yjc yjd. have hc: gle (psr S) (J (P i) (Q i)) (J (P i) (Q j)). rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. have hd: gle (psr S) (J (P i) (Q j)) (J (P j) (Q j)). rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or2); rewrite sr2. rewrite (yjd _ _ leI) /prl_dl_glam_fam LgV//; aw. rewrite -[in J i j] pj -[in (J i (J (P j) (Q j)))] pi. rewrite (prl_prop3 hc hd) //. move: (yjc _ j1I); rewrite /prl_dl_Elam_fam LgV//. exists x; first by apply/prl_limitP. rewrite/prl_dl_slice2/prl_dl_slice /x. apply:fgraph_exten; aww. rewrite yb => l lL; move:(yc _ lL); move: lL; simpl => lL. rewrite /prl_dl_F_lambda ! LgV//; move/prl_limitP => [yla ylb ylc yld]. have ha:psI (prl_dl_system_S_lambda l) = I1. by rewrite /prl_dl_system_S_lambda; case: (ixm (inc l I2)). rewrite ha in ylb. apply:fgraph_exten; fprops; rewrite ylb; aw; trivial. move => i iI2 /=; rewrite !LgV//; aw; trivial. by rewrite prl_dl_I; apply: setXp_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)