proposition: Lemma prl_dl2_res2: prl_map2_compat prl_dl2_limlim prl_dl2_limlim' prl_dl2_v_fam.
proof: Proof. rewrite /prl_dl2_v_fam; split. - fprops. - by aw. - move => i /= iI2; rewrite !LgV//. move:(prl_dl2_res1 iI2) => [ha hb]. exact: (proj1 (prl_map2_prop ha hb)). - move => i j /= leij'. move:(arg1_sr leij')(arg2_sr leij'); rewrite sr2 => iI2 jI2. rewrite !LgV // /prl_dl_hlm_gen; case: (ixm (inc (J i j) r2)) => // leij. clear leij'. set V := prl_dl2_v. set hlm := prl_dl_hlm or1 or2 sr1 sr2 Sr (pidl_i3_L or2 leij). set hlm' := prl_dl_hlm or1 or2 sr1 sr2 Sr' (pidl_i3_L or2 leij). move:(prl_dl2_res1 iI2)(prl_dl2_res1 jI2) =>[ha hb][ha' hb']. move: (prl_map2_prop3 ha hb) (prl_map2_prop3 ha' hb'). simpl. rewrite -/(prl_dl2_v _) -/(prl_dl2_v _) -/V. set Si := projective_limit _; set Si' := projective_limit _. set Sj := projective_limit _; set Sj' := projective_limit _. move => [[fvi svi tvi] Vip] [[fvj svj tvj] Vjp]. set T := prl_dl_S_lambda or1 or2 sr1 sr2 Sr. set T' := prl_dl_S_lambda or1 or2 sr1 sr2 Sr'. have sid1:prl_same_index (T _ (pidl_i2_L sr2 leij)) (T _ (pidl_i1_L sr2 leij)) by []. set QQ := prl_dl_halm_compat or1 or2 sr1 sr2. move: (prl_map2_prop3 sid1 (QQ _ Sr _ _ leij)). simpl; rewrite /T -/(prl_dl_hlm _ _ _ _ _ _) prl_dl_hml_invariant. have ->: (prl_dl_hlm_gen or1 or2 sr1 sr2 Sr (J i j)) = hlm. by rewrite /hlm prl_dl_hml_invariant; aw. rewrite -prl_dl_F_lambda_prop -prl_dl_F_lambda_prop. rewrite /prl_dl_F_lambda -/Si - /Sj. move => [[fLa sLa tLa] Lap]. have sid2:prl_same_index (T' _ (pidl_i2_L sr2 leij)) (T' _ (pidl_i1_L sr2 leij)) by []. move:(prl_map2_prop3 sid2 (QQ _ Sr' _ _ leij)). simpl; rewrite /T -/(prl_dl_hlm _ _ _ _ _ _) prl_dl_hml_invariant. have ->: (prl_dl_hlm_gen or1 or2 sr1 sr2 Sr' (J i j)) = hlm'. by rewrite /hlm' prl_dl_hml_invariant; aw. rewrite -prl_dl_F_lambda_prop -prl_dl_F_lambda_prop. rewrite /prl_dl_F_lambda -/Si' - /Sj'. move => [[fLb sLb tLb] Lbp]. have res1: V i \coP hlm by split => //; ue. have res2: hlm' \coP V j by split => //; ue. apply:function_exten. + by apply: compf_f. + by apply: compf_f. + aw; ue. + aw; ue. + aw; rewrite sLa => x xsj. have xs1:inc x (source (V j)) by ue. have xs2: inc x (source hlm) by ue. rewrite !compfV//. have qa: inc (Vf hlm x) Si by Wtac. have qb: inc (Vf (V i) (Vf hlm x)) Si' by Wtac. have qa': inc (Vf (V j) x) Sj' by Wtac. have qc: inc (Vf hlm' (Vf (V j) x)) Si' by Wtac; rewrite sLb; Wtac. move/prl_limitP: qb => [pa pb pc _]. move/prl_limitP: qc => [pa' pb' pc' _]. apply/fgraph_exten => //; first ue. have qe: psI (prl_dl2_Slambda i) = I1. rewrite /prl_dl2_Slambda /prl_dl_system_S_lambda. by case: (ixm (inc i I2)). have qe': psI (prl_dl2_Slambda' i) = I1. rewrite /prl_dl2_Slambda' /prl_dl_system_S_lambda. by case: (ixm (inc i I2)). move: pc';rewrite pb qe' => pc' k kI1. have kI2: inc k (psI (prl_dl2_Slambda i)) by ue. rewrite - (Lbp k _ kI1 qa') /prl_dl_halm_fam LgV//. have kI3 : inc k (psI (prl_dl2_Slambda j)). rewrite /prl_dl2_Slambda /prl_dl_system_S_lambda. by case: (ixm (inc j I2)). rewrite -(Vjp k _ kI3 xsj) - (Vip k (Vf hlm x) kI2 qa) /prl_dl2_ulam_fam. rewrite ! LgV// - (Lap _ _ kI1 xsj) /prl_dl_halm_fam LgV//. have le4: gle (psr S) (J k i) (J k j). rewrite Sr; apply/pidl_gleP1; split => //. by apply: (proj32 or1); rewrite sr1. move: (le4); rewrite Sr -Sr' => le4'. move:(prl_prop4 le4) =>[fkikj skikj tkikj]. move:(prl_prop4 le4') =>[fkikj' skikj' tkikj']. move:(prl_prop0 le4) => [le4a le4b]. move: (proj43 compat_u _ le4a) => [fui sui tui]. move: (proj43 compat_u _ le4b) => [fuj suj tuj]. have co2: Vg (psf S') (J (J k i) (J k j)) \coP Vg u (J k j) by split => //; ue. have co3: Vg u (J k i) \coP Vg (psf S) (J (J k i) (J k j)) by split => //; ue. have xs3: inc (Vg x k) (source (Vg u (J k j))). rewrite suj; move/prl_limitP: xsj => [_ _ h _]. move:(h k kI3); rewrite /prl_dl2_Slambda /prl_dl_system_S_lambda. case: (ixm (inc j I2)) => // H /=. rewrite /prl_dl_Elam_fam ! LgV//. have xs4: inc (Vg x k) (source (Vg (psf S) (J (J k i) (J k j)))). by rewrite skikj - suj. move:(proj44 compat_u (J k i) (J k j) le4) => cc. move:(f_equal (Vf ^~(Vg x k)) cc); rewrite !compfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)