proposition: Lemma prl_dl2_res3 (pl1 := projective_limit_fun S S' u) (pl2 := projective_limit_fun prl_dl2_limlim prl_dl2_limlim' prl_dl2_v_fam) (bij1 := prl_dl_can_iso or1 or2 sr1 sr2 Sr) (bij2 := prl_dl_can_iso or1 or2 sr1 sr2 Sr'): [/\ bijection bij1, bijection bij2 & pl2 \co bij1 = bij2 \co pl1].
proof: Proof. move:(prl_map2_prop3 psr_dl2_SrSr compat_u) => /=. rewrite -/pl1. set E := (projective_limit S); set E':= (projective_limit S'). move => [[fpl1 spl1 tpl1] pl1_prop]. have ha: prl_same_index prl_dl2_limlim prl_dl2_limlim' by []. move: (prl_map2_prop3 ha prl_dl2_res2); simpl. rewrite -/pl2. set vE:= projective_limit _; set vE':= projective_limit _. move => [[fpl2 spl2 tpl2] pl2_prop]. move:(prl_dl_canon_bijection or1 or2 sr1 sr2 Sr). move:(prl_dl_canon_bijection or1 or2 sr1 sr2 Sr'). rewrite -/bij1 -/bij2 -/E -/E' -/vE -/vE'. move => [bp2 sf2 tf2] [bp1 sf1 tf1]. split => //. move:(bp2)(bp1) => [[ff1 _] _] [[ff2 _] _]. have co1: pl2 \coP bij1 by split => //; ue. have co2: bij2 \coP pl1 by split => //; ue. apply: function_exten;try (apply: compf_f => //); aw; try ue. rewrite sf1 => x xE. have xs1: inc x (source pl1) by ue. have xs2: inc x (source bij1) by ue. have xs3:inc (Vf pl1 x) E' by Wtac. have ax1:lf_axiom (prl_dl_slice2 I1 I2) (projective_limit S') (projective_limit (prl_dl_systemS' or1 or2 sr1 sr2 Sr')). by apply:prl_dl_slice_p2. have ax2: lf_axiom (prl_dl_slice2 I1 I2) (projective_limit S) (projective_limit (prl_dl_systemS' or1 or2 sr1 sr2 Sr)). by apply:prl_dl_slice_p2. rewrite !compfV //. have xs4: inc (Vf bij1 x) vE by Wtac. have xs4': inc (Vf pl2 (Vf bij1 x)) vE' by Wtac. have xs5: inc (Vf bij2 (Vf pl1 x)) vE' by Wtac. move/(prl_limitP): xs4' => [qa qb qc _]. move/(prl_limitP): xs5 => [qa' qb' qc' _]. apply: fgraph_exten => //; first ue. rewrite qb => l /= lI2; clear qa qb qa' qb'. move: (qc l lI2); rewrite /= LgV//prl_dl_F_lambda_prop. move/(prl_limitP) => [ra rb _ _]. move: (qc' l lI2); rewrite /= LgV//prl_dl_F_lambda_prop. move/(prl_limitP) => [ra' rb' _ _]. apply/fgraph_exten => //; first ue. move => i; rewrite rb /= => iI1; clear ra rb ra' rb'. have ijI: inc (J i l) (psI S). rewrite - ps_substrate_r Sr. rewrite (proj2 (pidl_or or1 or2 sr1 sr2)); fprops. rewrite - (pl2_prop _ _ lI2 xs4). rewrite /bij1/bij2/prl_dl_can_iso. rewrite LfV// LfV//. rewrite/prl_dl_slice2 /prl_dl2_v_fam ! LgV// /prl_dl_slice. rewrite - (pl1_prop _ _ ijI xE). have iI3: inc i (psI (prl_dl2_Slambda l)). rewrite /prl_dl2_Slambda /prl_dl_system_S_lambda. by case: (ixm (inc l I2)). have sl: inc (prl_dl_slice I1 x l) (projective_limit (prl_dl2_Slambda l)). by apply:(prl_dl_slice_p1). move: (prl_dl2_res1 lI2) => [hax hbx]. rewrite - (proj2 (prl_map2_prop3 hax hbx) _ _ iI3 sl). rewrite/prl_dl2_ulam_fam/prl_dl_slice !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)