proposition: Lemma prl_dl_hml_id i: inc i I2 -> Vg (Lg r2 prl_dl_hlm_gen) (J i i) = identity (prl_dl_F_lambda i).
proof: Proof. move => i2. have iir: inc (J i i) r2 by apply: (proj32 or2 i); rewrite sr2. rewrite LgV // prl_dl_F_lambda_prop. set S1 := (prl_dl_S_lambda (pidl_i1_L sr2 iir)). set S2 := (prl_dl_S_lambda (pidl_i2_L sr2 iir)). have ha: (prl_same_index S1 S2) by []. have hb:=(prl_dl_halm_compat iir). move:(prl_map2_prop ha hb). set f := projective_limit_fun _ _ _. have <-: f = prl_dl_hlm_gen (J i i) by apply:(prl_dl_hml_invariant iir). move => [[ff sf tf] fp]. apply:function_exten. - done. - fprops. - by aw. - by aw. - rewrite sf => x xl; rewrite idV //. have fxl: inc (Vf f x) (projective_limit S2) by Wtac. move/prl_limitP: (xl) => [xa xb xc xd]. move/prl_limitP: fxl => [xa' xb' xc' xd']. apply: fgraph_exten => //; rewrite ? xb xb' // => j jI2. move:(prl_map_val_aux2 ha hb jI2 xl). have hu: inc (J j i) (psI S) by rewrite prl_dl_I; apply/setXp_i. move: (prl_dl_S_lambda_prop (pidl_i1_L sr2 iir)). rewrite -/S1. move => [s1E s1I s1r s1f]. have h1: inc (Vg x j) (Vg (psE S) (J j i)). by move:(xc _ jI2); rewrite s1E /prl_dl_Elam_fam LgV//. have ji1: inc j I1 by rewrite - s1I. rewrite /prl_dl_halm_fam (LgV jI2) (prl_prop5 hu h1). by rewrite - (prl_map_val_aux2 ha (prl_dl_halm_compat iir) jI2 xl). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)